PFR/ForMathlib/ThreeVariables.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. lemma ProbabilityTheory.iIndepFun.reindex_three_abc line 19 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume

    4 instances, coercions and auxiliary constants left out.

  2. lemma ProbabilityTheory.iIndepFun.reindex_three_acb line 22 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume

    Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail and 12 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  3. lemma ProbabilityTheory.iIndepFun.reindex_three_bac line 34 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume

    Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail and 12 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  4. lemma ProbabilityTheory.iIndepFun.reindex_three_bca line 46 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume

    Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail and 12 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  5. lemma ProbabilityTheory.iIndepFun.reindex_three_cab line 58 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume

    Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail and 12 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  6. lemma ProbabilityTheory.iIndepFun.reindex_three_cba line 70 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume

    Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail and 12 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  7. abbrev ProbabilityTheory.iIndepFun.κ line 82 source

    Distinct definitions of this name: PFR/ForMathlib/FourVariables.lean:237 (different declaration text). Qualify references as ProbabilityTheory.iIndepFun.κ@path.

  8. def ProbabilityTheory.iIndepFun.κ_equiv line 86 source

    Distinct definitions of this name: PFR/ForMathlib/FourVariables.lean:241 (different declaration text). Qualify references as ProbabilityTheory.iIndepFun.κ_equiv@path.

  9. instance ProbabilityTheory.iIndepFun.fintype_kappa line 96 source

    Distinct definitions of this name: PFR/ForMathlib/FourVariables.lean:252 (different declaration text). Qualify references as ProbabilityTheory.iIndepFun.fintype_kappa@path.

  10. abbrev ProbabilityTheory.iIndepFun.self_or_prod line 100 source
  11. lemma ProbabilityTheory.iIndepFun.pair_last_of_three line 104 source

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

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IndepFun, Prod, prod

    Proof uses: Equiv, Sigma, Sigma.mk, ProbabilityTheory.iIndepFun.pi', List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, eq_of_heq and 20 more

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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