lowerSemicontinuousOn_indicator — Mathlib

English

If s is closed and y ≤ 0, then the indicator function of s is lower semicontinuous on the whole space.

Русский

Если s замкнуто, и y ≤ 0, то индикатор s — нижняя полупрерывность на всём пространстве.

LaTeX

$$$\operatorname{LowerSemicontinuousOn}(\mathbf{1}_{s} \cdot y, t)$$$

Lean4

theorem lowerSemicontinuousOn_indicator (hs : IsClosed s) (hy : y ≤ 0) :
    LowerSemicontinuousOn (indicator s fun _x => y) t :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousOn t

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