lowerSemicontinuous_iff_isClosed_epigraph

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]

Похожие утверждения