Theorems · Theorem · measure theory

MeasureTheory.inducedOuterMeasure_zero

∀ {α : Type u_1} {P : Set α → Prop} {P0 : P ∅},
  (∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) →
    P Set.univ →
      MeasureTheory.inducedOuterMeasure (fun x x_1 => 0) P0 MeasureTheory.inducedOuterMeasure_zero._proof_1 = 0

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

1 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound