PFR/Mathlib/MeasureTheory/Constructions/Pi.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. instance MeasureTheory.Measure.(instance at line 13) line 13 source
  2. lemma MeasureTheory.Measure.pi_pi_set line 17 source

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

    Statement uses: Fintype, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Set, DecidablePred, Membership.mem, Eq, ENNReal, MeasureTheory.Measure.pi, Set.pi, Finset.prod, Finset.filter, Finset.univ

    Proof uses: Eq.mpr, Set.univ, ite, id, congrFun', congrArg, MeasureTheory.Measure.pi_pi, Finset.prod_congr, Eq.refl, Finset, apply_ite, OfNat.ofNat, ite_congr, Not, MeasureTheory.IsProbabilityMeasure.measure_univ, HMul.hMul, Finset.prod_ite, Finset.prod_const_one, of_eq_true, Eq.trans and 3 more

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. lemma MeasureTheory.Measure.pi_eval_preimage line 25 source

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

    Statement uses: Fintype, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Set, Eq, ENNReal, MeasureTheory.Measure.pi, Set.preimage, Function.eval

    Proof uses: Eq.mpr, Set.pi, Set.univ, Function.update, Classical.propDecidable, id, congrFun', congrArg, Set.eval_preimage, Finset.prod, Finset.univ, MeasureTheory.Measure.pi_pi, Finset.prod_congr, Eq.refl, Finset, Membership.mem, Function.apply_update, OfNat.ofNat, Function.update_congr, funext and 14 more

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. lemma MeasureTheory.Measure.map_eval_pi line 31 source

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

    Statement uses: Fintype, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Eq, MeasureTheory.Measure.map, Function.eval, MeasureTheory.Measure.pi

    Proof uses: MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, ENNReal, Set.preimage, id, congrFun', congrArg, MeasureTheory.Measure.map_apply, measurable_pi_apply, of_eq_true, Eq.trans, True, MeasureTheory.Measure.pi_eval_preimage, eq_self

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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