lowerSemicontinuousOn_iff_le_liminf

English

Let f: α → γ. The function is lower semicontinuous on a set s if and only if for every x ∈ s, f(x) ≤ liminf f(𝓝[s] x).

Русский

Пусть f: α → γ. Функция ниже полупрерывна на множестве s тогда и только тогда, когда для каждого x ∈ s выполняется f(x) ≤ liminf f(𝓝[s] x).

LaTeX

$$$\\text{LowerSemicontinuousOn} f\\,s \\iff \\forall x \\in s,\\; f(x) \\le \\liminf f(\\mathcal{N}_s x)$$$

Lean4

theorem lowerSemicontinuousOn_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x) := by
  simp only [← lowerSemicontinuousWithinAt_iff_le_liminf, LowerSemicontinuousOn]

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