upperSemicontinuous_const

Mathlib.Topology.Semicontinuous

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

English

A constant function is upper semicontinuous as a global function.

Русский

Константная функция верхнеполупрерывна как функция на всём пространстве.

LaTeX

$$$\\mathrm{UpperSemicontinuous}(\\lambda\\_, z)$$$

Lean4

theorem upperSemicontinuous_const : UpperSemicontinuous fun _x : α => z := fun _x => upperSemicontinuousAt_const

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

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

Разделы

Аффилиация

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