upperSemicontinuousWithinAt_indicator

English

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

Русский

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

LaTeX

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

Lean4

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

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