upperSemicontinuousAt_iff_limsup_le

English

Upper semicontinuity at a point is equivalent to the limsup inequality at that point.

Русский

Верхняя полупрерывность в точке эквивалентна неравенству limsup в этой точке.

LaTeX

$$$\\mathrm{UpperSemicontinuousAt}(f,x) \\iff \\limsup f (\\mathcal{N}(x)) \\le f(x)$$$

Lean4

theorem upperSemicontinuousAt_iff_limsup_le {f : α → γ} : UpperSemicontinuousAt f x ↔ limsup f (𝓝 x) ≤ f x :=
  lowerSemicontinuousAt_iff_le_liminf (γ := γᵒᵈ)

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