measure_eq_iInf' — Mathlib

English

A variant of measure_eq_iInf' using a single index set for t.

Русский

Вариант measure_eq_iInf' с единичной индексной множеством t.

LaTeX

$$$\mu s = \iInf t : { t \;|\; s \subseteq t \land MeasurableSet t }, \mu t$$$

Lean4

/-- A variant of `measure_eq_iInf` which has a single `iInf`. This is useful when applying a
  lemma next that only works for non-empty infima, in which case you can use
  `nonempty_measurable_superset`. -/
theorem measure_eq_iInf' (μ : Measure α) (s : Set α) : μ s = ⨅ t : { t // s ⊆ t ∧ MeasurableSet t }, μ t := by
  simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]

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