essInf_congr_ae

Mathlib.MeasureTheory.Function.EssSup

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

English

For general β with linear order, essInf f μ equals the sInf of a family defined by threshold comparisons.

Русский

Для обобщенного β линейного порядка essInf равен sInf семейства порогов.

LaTeX

$$$ues sInf {a | μ {x | f x < a} = 0}$.$$

Lean4

theorem essInf_congr_ae {f g : α → β} (hfg : f =ᵐ[μ] g) : essInf f μ = essInf g μ :=
  @essSup_congr_ae α βᵒᵈ _ _ _ _ _ hfg

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

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

Разделы

Аффилиация

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