upperSemicontinuousWithinAt — Mathlib

English

If f is upper semicontinuous, then for any set s and any x, f is upper semicontinuous within s at x.

Русский

Если f имеет верхнюю полупрерывность, то для произвольного множества s и точки x функция f ограниченная на s остается верхнеполупрерывной в точке x.

LaTeX

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

Lean4

theorem upperSemicontinuousWithinAt (h : UpperSemicontinuous f) (s : Set α) (x : α) :
    UpperSemicontinuousWithinAt f s x :=
  (h x).upperSemicontinuousWithinAt s

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