essSup_const_bot

Mathlib.MeasureTheory.Function.EssSup

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

English

essSup of a constant bottom function is bottom: essSup (const bottom) μ = bottom.

Русский

эссСуп константы ⊥ равен ⊥.

LaTeX

$$$$ \\operatorname{essSup} (\\lambda x. \\perp) \\mu = \\perp $$$$

Lean4

theorem essSup_const_bot : essSup (fun _ : α => (⊥ : β)) μ = (⊥ : β) :=
  limsup_const_bot

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

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

Разделы

Аффилиация

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