trim_eq_iInf' — Mathlib

English

A variant expression: the trim equals the infimum over all measurable t with s ⊆ t, expressed via a subtype-indexed infimum.

Русский

Вариант выражения: обрезка равна инфимууму над измеримыми t с условием s ⊆ t, выраженному через инфимуум по подтипу.

LaTeX

$$$$ m^{\mathrm{trim}}(s) = \inf_{t \;:\; s \subseteq t,\ MeasurableSet(t)} m(t). $$$$

Lean4

theorem trim_eq_iInf' (s : Set α) : m.trim s = ⨅ t : { t // s ⊆ t ∧ MeasurableSet t }, m t := by
  simp [iInf_subtype, iInf_and, trim_eq_iInf]

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