upperSemicontinuousWithinAt_iff_limsup_le

English

WithinAt USC is equivalent to limsup ≤ f(x) along nhds within s.

Русский

USC внутри по отношению к s эквивалентна limsup ≤ f(x) вдоль nhds внутри s.

LaTeX

$$$\\mathrm{UpperSemicontinuousWithinAt}(f,s,x) \\iff \\limsup f (\\mathcal{N}_s(x)) \\le f(x)$$$

Lean4

theorem upperSemicontinuousWithinAt_iff_limsup_le {f : α → γ} :
    UpperSemicontinuousWithinAt f s x ↔ limsup f (𝓝[s] x) ≤ f x :=
  lowerSemicontinuousWithinAt_iff_le_liminf (γ := γᵒᵈ)

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