lowerSemicontinuousWithinAt_indicator

English

If s is open and y ≥ 0, then the indicator function of s is lower semicontinuous within any t at x.

Русский

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

LaTeX

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

Lean4

theorem lowerSemicontinuousWithinAt_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuousWithinAt (indicator s fun _x => y) t x :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousWithinAt t x

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