upperSemicontinuousOn_iff_limsup_le

English

Let f: α → γ and s ⊆ α. The function f is upper semicontinuous on s if and only if for every x ∈ s, the limsup of f over the neighborhood filter nhdsWithin x s is at most f(x).

Русский

Пусть f: α → γ и s ⊆ α. Функция f верхняя полупрерывна на s тогда и только тогда, когда для каждого x ∈ s limsup f над nhdsWithin x s не превосходит f(x).

LaTeX

$$$\\text{UpperSemicontinuousOn}(f,s) \\iff \\forall x\\in s, \\ \\limsup f(\\nhdsWithin x s) \\le f(x).$$$

Lean4

theorem upperSemicontinuousOn_iff_limsup_le {f : α → γ} :
    UpperSemicontinuousOn f s ↔ ∀ x ∈ s, limsup f (𝓝[s] x) ≤ f x :=
  lowerSemicontinuousOn_iff_le_liminf (γ := γᵒᵈ)

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