lowerSemicontinuousWithinAt_const

English

The constant function z is lower semicontinuous within any set s at any x.

Русский

Постоянная функция z имеет нижнюю полупрерывность внутри любого множества s в любой точке x.

LaTeX

$$$\operatorname{LowerSemicontinuousWithinAt}(\lambda\,x. z, s, x)$$$

Lean4

theorem lowerSemicontinuousWithinAt_const : LowerSemicontinuousWithinAt (fun _x => z) s x := fun _y hy =>
  Filter.Eventually.of_forall fun _x => hy

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