upperSemicontinuousAt_indicator — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem upperSemicontinuousAt_indicator (hs : IsClosed s) (hy : 0 ≤ y) :
    UpperSemicontinuousAt (indicator s fun _x => y) x :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousAt x

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