essInf_const_top

Mathlib.MeasureTheory.Function.EssSup

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

English

essInf of a constant top function is top: essInf (const top) μ = top.

Русский

эссИнф константы ⊤ равен ⊤.

LaTeX

$$$$ \\operatorname{essInf} (\\lambda x. \\top) \\mu = \\top $$$$

Lean4

theorem essInf_const_top : essInf (fun _ : α => (⊤ : β)) μ = (⊤ : β) :=
  liminf_const_top

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

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

Разделы

Аффилиация

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