lowerSemicontinuousAt_iff_le_liminf

English

Let f: α → γ be a function into a complete linear order γ. Then f is lower semicontinuous at x if and only if f(x) ≤ liminf f(𝓝 x).

Русский

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

LaTeX

$$$\\text{LowerSemicontinuousAt} \\\\ f \\\\ x \\\\iff f(x) \\\\le \\\\liminf f \\\\ left( 𝓝 x \\right)$$$

Lean4

theorem lowerSemicontinuousAt_iff_le_liminf {f : α → γ} : LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x) := by
  rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf, ← nhdsWithin_univ]

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