English
If s is closed and f : α → γ, then f is lower semicontinuous on s if and only if the set of points (x, t) with x ∈ s and f(x) ≤ t is closed in α × γ.
Русский
Если s замкнуто, то функция f: α → γ является нижней полупрерывной на s тогда и только тогда множество пар (x, t) с x ∈ s и f(x) ≤ t закрыто в α × γ.
LaTeX
$$$\\text{LowerSemicontinuousOn} \\\\ f \\\\ s \\iff \\text{IsClosed} \\\\{ p=(x,t) ∈ α×γ \\mid x∈s ∧ f(x) ≤ t \\}$$$
Lean4
theorem lowerSemicontinuousOn_iff_isClosed_epigraph {f : α → γ} {s : Set α} (hs : IsClosed s) :
LowerSemicontinuousOn f s ↔ IsClosed {p : α × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
by
simp_rw [LowerSemicontinuousOn, LowerSemicontinuousWithinAt, eventually_nhdsWithin_iff, ← isOpen_compl_iff,
compl_setOf, isOpen_iff_eventually, mem_setOf, not_and, not_le]
constructor
· intro hf ⟨x, y⟩ h
by_cases hx : x ∈ s
· have ⟨y', hy', z, hz, h₁⟩ := (h hx).exists_disjoint_Iio_Ioi
filter_upwards [(hf x hx z hz).prodMk_nhds (eventually_lt_nhds hy')] with _ ⟨h₂, h₃⟩ h₄ using h₁ _ h₃ _ <| h₂ h₄
·
filter_upwards [(continuous_fst.tendsto _).eventually (hs.isOpen_compl.eventually_mem hx)] with _ h₁ h₂ using
(h₁ h₂).elim
· intro hf x _ y hy
exact ((Continuous.prodMk_left y).tendsto x).eventually (hf (x, y) (fun _ => hy))
