lowerSemicontinuous_iff_le_liminf

English

For a function f: α → γ, f is lower semicontinuous if and only if, for every x, f(x) ≤ liminf f(𝓝 x).

Русский

Для функции f: α → γ выполняется равенство: f является нижней полупрерывной тогда и только тогда, когда для каждого x выполняется f(x) ≤ liminf f(𝓝 x).

LaTeX

$$$\\text{LowerSemicontinu} f \\iff \\forall x, f(x) \\le \\liminf f(𝓝 x)$$$

Lean4

theorem lowerSemicontinuous_iff_le_liminf {f : α → γ} : LowerSemicontinuous f ↔ ∀ x, f x ≤ liminf f (𝓝 x) := by
  simp only [← lowerSemicontinuousAt_iff_le_liminf, LowerSemicontinuous]

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