essSup_count

Mathlib.MeasureTheory.Function.EssSup

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

English

If μ assigns positive mass to every singleton, then essInf f μ equals the infimum over i of f(i).

Русский

Если μ положительно распределяет массу по каждой точке, то essInf f μ = inf_i f(i).

LaTeX

$$$$ \\operatorname{essInf} f \\mu = \\bigwedge_{i} f(i) $$$$

Lean4

@[simp]
theorem essSup_count [MeasurableSingletonClass α] (f : α → β) : essSup f .count = ⨆ i, f i :=
  essSup_eq_iSup (by simp) _

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

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

Разделы

Аффилиация

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