Lowersemicontinuous Functions have Closed Epigraphs

Stream: mathlib4

[Yongxi Lin (Aaron)]

Given a lowersemicontinuous function $\phi:X\rightarrow \mathbb{R}$ defined on some topological space $X$. I want to prove that its epigraph $\{(x,s)\in X\times \mathbb{R}|\phi(x)\leq s\}$ is closed in $X\times \mathbb{R}$ in lean. I want to use this theorem LowerSemicontinuous.isClosed_epigraph, but as $\mathbb{R}$ does not have a complete linear order, I need to first make $\phi$ a function from $X$ to $[-\infty,\infty]$. Even if I did this, this existing theorem in mathlib can only give me IsClosed $\{(x,s)\in X\times [-\infty,\infty]|\phi(x)\leq s\}$ instead of IsClosed $\{(x,s)\in X\times \mathbb{R}|\phi(x)\leq s\}$. Does anybody know a better way to solve this issue?

[Aaron Liu]

I think once you have that IsClosed $\{(x,s)\in X\times [-\infty,\infty]|\phi(x)\leq s\}$ you can use docs#IsClosed.preimage to get that IsClosed $\{(x,s)\in X\times \mathbb{R}|\phi(x)\leq s\}$ using the fact that the embedding from reals to ereals is continuous.

[Alex Nguyen]

I had to prove something like this. My approach was like this, apologies that it's probably not the most elegant code possible

import Mathlib
open TopologicalSpace

lemma closedepigraph_of_lsc {X : Type*} [TopologicalSpace X]
    {φ : X → ℝ} (hφ_lsc : LowerSemicontinuous φ) :
    IsClosed {p : X × ℝ | φ p.1 ≤ p.2}  := by
  let C := {p : X × ℝ | φ p.1 ≤ p.2}

  have hC_closed : IsClosed C := by
    let g : X × ℝ → ℝ := fun p => φ p.1 - p.2
    have hg_lsc : LowerSemicontinuous g := by
      intro p
      apply LowerSemicontinuousAt.add'
      · exact LowerSemicontinuousAt.comp_continuousAt (hφ_lsc p.1) continuous_fst.continuousAt
      · exact (continuous_neg.comp continuous_snd).lowerSemicontinuous p
      · exact continuous_add.continuousAt

    have hC_eq_preimage : C = g⁻¹' (Set.Iic 0) := by
      ext p; simp [g]; rfl
    rw [hC_eq_preimage]
    apply hg_lsc.isClosed_preimage
  exact hC_closed

[Yongxi Lin (Aaron)]

Thank you both for your help.