upperSemicontinuousOn_indicator — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem upperSemicontinuousOn_indicator (hs : IsClosed s) (hy : 0 ≤ y) :
    UpperSemicontinuousOn (indicator s fun _x => y) t :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousOn t

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