upperSemicontinuous — Mathlib

English

If f is continuous within s at x, then f is upper semicontinuous within s at x (alternative statement).

Русский

Если f непрерывна внутри s в x, то она USC внутри s в x (альтернативное выражение).

LaTeX

$$$\\mathrm{ContinuousWithinAt}(f,s,x) \\Rightarrow \\mathrm{UpperSemicontinuousWithinAt}(f,s,x)$$$

Lean4

theorem upperSemicontinuous {f : α → γ} (h : Continuous f) : UpperSemicontinuous f := fun _x =>
  h.continuousAt.upperSemicontinuousAt

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