upperSemicontinuous_iff_limsup_le

English

Let f be a function from a topological space into a complete linear order γ. Then f is upper semicontinuous if and only if for every x, the limit superior of f at x does not exceed f(x); equivalently, limsup f (nhds x) ≤ f(x) for all x.

Русский

Пусть f: α → γ, где γ есть полный линейный порядок. Тогда f имеет верхнюю полупрерывность тогда и только тогда, когда для каждой точки x верно limsup(f, x) ≤ f(x); эквивалентно limsup f (nhds x) ≤ f(x) для всех x.

LaTeX

$$$\\text{UpperSemicontinuous}(f) \\iff \\forall x, \\limsup f(\\mathcal{N}x) \\le f(x)$.$$

Lean4

theorem upperSemicontinuous_iff_limsup_le {f : α → γ} : UpperSemicontinuous f ↔ ∀ x, limsup f (𝓝 x) ≤ f x :=
  lowerSemicontinuous_iff_le_liminf (γ := γᵒᵈ)

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