upperSemicontinuousWithinAt_indicator

English

If s is open and y ≤ 0, then χ_s(y) is upper semicontinuous within t at x.

Русский

Если s открыто и y ≤ 0, χ_s(y) верхнеполупрерывна внутри t в точке x.

LaTeX

$$$\\mathrm{IsOpen}(s) \\land y \\le 0 \\Rightarrow \\mathrm{UpperSemicontinuousWithinAt}(\\mathrm{indicator}(s, \\lambda x. y), t, x)$$$

Lean4

theorem upperSemicontinuousWithinAt_indicator (hs : IsOpen s) (hy : y ≤ 0) :
    UpperSemicontinuousWithinAt (indicator s fun _x => y) t x :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousWithinAt t x

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