upperSemicontinuousWithinAt_const

English

A constant function is upper semicontinuous within any set s and at any point x.

Русский

Константная функция на любом множестве внутри обладает верхней полупрерывностью в любой точке.

LaTeX

$$$\\mathrm{UpperSemicontinuousWithinAt}(\\lambda\\_, z)\u200b\, s\\ x$$$

Lean4

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

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