lowerSemicontinuousAt

Mathlib.Topology.Semicontinuous

URI: https://scilib.ai/kg/mathlib#LowerSemicontinuous.lowerSemicontinuousAt

English

If f is lower semicontinuous, then f is lower semicontinuous at every point x.

Русский

Пусть f — нижняя полупрерывная функция. Тогда f является нижней полупрерывной в каждой точке x.

LaTeX

$$$\operatorname{LowerSemicontinuousAt}(f, x)$$$

Lean4

theorem lowerSemicontinuousAt (h : LowerSemicontinuous f) (x : α) : LowerSemicontinuousAt f x :=
  h x

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

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

Разделы

Аффилиация

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