PFR/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

TODO

Rename setLIntegral_congr to setLIntegral_congr_set

Imports (1)
Imported by 2 files
  1. lemma MeasureTheory.lintegral_eq_zero_of_ae_zero line 18 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ENNReal, Eq, Compl.compl, OfNat.ofNat, Membership.mem, MeasurableSet, MeasureTheory.lintegral

    Proof uses: Eq.mpr, HAdd.hAdd, MeasureTheory.Measure.restrict, id, congrArg, Eq.symm, MeasureTheory.lintegral_add_compl, MeasureTheory.setLIntegral_measure_zero, MeasureTheory.setLIntegral_congr_fun, of_eq_true, Eq.trans, True, congrFun', HMul.hMul, Set.univ, MeasureTheory.lintegral_const, Inter.inter, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MulZeroClass.zero_mul and 2 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. lemma MeasureTheory.lintegral_eq_setLIntegral line 24 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Eq, ENNReal, Compl.compl, OfNat.ofNat, MeasureTheory.lintegral, MeasureTheory.Measure.restrict

    Proof uses: Eq.mpr, Set.univ, id, congrArg, Eq.symm, MeasureTheory.setLIntegral_univ, MeasureTheory.setLIntegral_congr, Filter.EventuallyEqSet, MeasureTheory.ae, propext, MeasureTheory.ae_eq_univ, Eq.refl

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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