upperSemicontinuousOn — Mathlib

English

If f is upper semicontinuous, then f is upper semicontinuous on any subset s.

Русский

Если f верхнеполупрерывна, то она верхнеполупрерывна на любом подмножестве s.

LaTeX

$$$\\mathrm{UpperSemicontinuous}(f) \\Rightarrow \\forall s, \\mathrm{UpperSemicontinuousOn}(f,s)$$$

Lean4

theorem upperSemicontinuousOn (h : UpperSemicontinuous f) (s : Set α) : UpperSemicontinuousOn f s := fun x _hx =>
  h.upperSemicontinuousWithinAt s x

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