English
For γ a linear order with appropriate topology, LowerSemicontinuous f is equivalent to the epigraph { (x,t) | f(x) ≤ t } being closed in α × γ.
Русский
Для линейного порядка γ с подходящей топологией, нижняя полупрерывность функции f эквивалентна тому, что эпиграф { (x,t) | f(x) ≤ t } замкнут в пространствах α × γ.
LaTeX
$$$\\text{LowerSemicontinuous} f \\iff \\text{IsClosed} \\{ (x,t) ∈ α×γ \\mid f(x) ≤ t \\}$$$
Lean4
theorem lowerSemicontinuous_iff_isClosed_epigraph {f : α → γ} :
LowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2} := by
simp [← lowerSemicontinuousOn_univ_iff, lowerSemicontinuousOn_iff_isClosed_epigraph]