lowerSemicontinuousAt_indicator — Mathlib

English

If s is open and y ≥ 0, then the indicator function of s is lower semicontinuous at a given point.

Русский

Если s открыто, и y ≥ 0, то индикаторная функция s имеет нижнюю полупрерывность в данной точке.

LaTeX

$$$\operatorname{LowerSemicontinuousAt}(\mathbf{1}_{s} \cdot y, x)$$$

Lean4

theorem lowerSemicontinuousAt_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuousAt (indicator s fun _x => y) x :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousAt x

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