exists_measurable_superset_forall_eq

English

A variant of measure_eq_iInf' using a single iInf.

Русский

Вариант measure_eq_iInf' с единым iInf.

LaTeX

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

Lean4

/-- For every set `s` and a countable collection of measures `μ i` there exists a measurable
superset `t ⊇ s` such that each measure `μ i` takes the same value on `s` and `t`. -/
theorem exists_measurable_superset_forall_eq [Countable ι] (μ : ι → Measure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ i, μ i t = μ i s := by
  simpa only [← measure_eq_trim] using
    OuterMeasure.exists_measurable_superset_forall_eq_trim (fun i => (μ i).toOuterMeasure) s

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