essInf_eq_iInf — Mathlib

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

theorem essInf_eq_iInf (hμ : ∀ a, μ { a } ≠ 0) (f : α → β) : essInf f μ = ⨅ i, f i := by
  rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]

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