upperSemicontinuousAt_const

Mathlib.Topology.Semicontinuous

URI: https://scilib.ai/kg/mathlib#upperSemicontinuousAt_const

English

A constant function is upper semicontinuous at every point x.

Русский

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

LaTeX

$$$\\mathrm{UpperSemicontinuousAt}(\\lambda\\_, z)\\, x$$$

Lean4

theorem upperSemicontinuousAt_const : UpperSemicontinuousAt (fun _x => z) x := fun _y hy =>
  Filter.Eventually.of_forall fun _x => hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru