PFR/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 3 files
  1. lemma MeasureTheory.measure_eq_univ_of_forall_singleton line 14 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasureTheory.Measure, Set, Membership.mem, Compl.compl, Eq, ENNReal, Singleton.singleton, OfNat.ofNat, Set.univ

    Proof uses: le_antisymm, MeasureTheory.measure_mono, Set.subset_univ, Eq.mpr, LE.le, Union.union, id, congrArg, Eq.symm, Set.union_compl_self, LE.le.trans, HAdd.hAdd, MeasureTheory.measure_union_le, Iff.mpr, MeasureTheory.measure_null_iff_singleton, Set.to_countable, of_eq_true, Eq.trans, True, congrFun' and 1 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.