Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

10 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 3 files
  1. theorem AddCircle.liftIco_coe_apply_of_periodic line 30 source

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle.liftIco, AddSubgroup.zmultiples

    Proof uses: Eq.mpr, Function.comp, AddCircle, Set.Ico, HAdd.hAdd, Set.domRestrict, Equiv, AddCircle.equivIco, id, congrArg, AddCircle.liftIco.eq_1, QuotientAddGroup.equivIcoMod, AddCircle.equivIco.eq_1, Function.comp_apply, Membership.mem, Set, Set.domRestrict_apply, Subtype.mk, toIcoMod, toIcoMod_mem_Ico and 13 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. theorem AddCircle.liftIoc_coe_apply_of_periodic line 34 source

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle.liftIoc, AddSubgroup.zmultiples

    Proof uses: Eq.mpr, Function.comp, AddCircle, Set.Ioc, HAdd.hAdd, Set.domRestrict, Equiv, AddCircle.equivIoc, id, congrArg, AddCircle.liftIoc.eq_1, QuotientAddGroup.equivIocMod, AddCircle.equivIoc.eq_1, Function.comp_apply, Membership.mem, Set, Set.domRestrict_apply, Subtype.mk, toIocMod, toIocMod_mem_Ioc and 13 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  3. theorem AddCircle.liftIco_comp_mk_eq_of_periodic line 38 source

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, Function.comp, AddCircle, AddCircle.liftIco, AddSubgroup.zmultiples

    Proof uses: funext, AddCircle.liftIco_coe_apply_of_periodic

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. theorem AddCircle.liftIoc_comp_mk_eq_of_periodic line 41 source

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, Function.comp, AddCircle, AddCircle.liftIoc, AddSubgroup.zmultiples

    Proof uses: funext, AddCircle.liftIoc_coe_apply_of_periodic

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  5. theorem AddCircle.liftIco_eq_liftIco If f has period p, then every lift of f to AddCircle p is the same line 45 source

    Source documentation

    If f has period p, then every lift of f to AddCircle p is the same.

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle, AddCircle.liftIco

    Proof uses: funext, QuotientAddGroup.induction_on, AddSubgroup.zmultiples, of_eq_true, Eq.trans, True, congr, congrArg, AddCircle.liftIco_coe_apply_of_periodic, eq_self

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem liftIco_eq_liftIco : liftIco p a f = liftIco p a' f :=
…
  6. theorem AddCircle.liftIoc_eq_liftIoc If f has period p, then every lift of f to AddCircle p is the same line 50 source

    Source documentation

    If f has period p, then every lift of f to AddCircle p is the same.

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle, AddCircle.liftIoc

    Proof uses: funext, QuotientAddGroup.induction_on, AddSubgroup.zmultiples, of_eq_true, Eq.trans, True, congr, congrArg, AddCircle.liftIoc_coe_apply_of_periodic, eq_self

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem liftIoc_eq_liftIoc : liftIoc p a f = liftIoc p a' f :=
…
  7. theorem AddCircle.liftIco_eq_liftIoc If f has period p, then every lift of f to AddCircle p is the same line 55 source

    Source documentation

    If f has period p, then every lift of f to AddCircle p is the same.

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

    Statement uses: AddCommGroup, LinearOrder, IsOrderedAddMonoid, Archimedean, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle, AddCircle.liftIco, AddCircle.liftIoc

    Proof uses: funext, QuotientAddGroup.induction_on, AddSubgroup.zmultiples, Eq.mpr, id, congrArg, AddCircle.liftIco_coe_apply_of_periodic, AddCircle.liftIoc_coe_apply_of_periodic, Eq.refl

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem liftIco_eq_liftIoc : liftIco p a f = liftIoc p a' f :=
…
  8. lemma AddCircle.equivAddCircle_eq line 67 source

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

    Statement uses: Field, LinearOrder, IsStrictOrderedRing, Archimedean, Fact, LT.lt, OfNat.ofNat, Eq, AddCircle, AddEquiv, AddSubgroup.zmultiples, AddCircle.equivAddCircle, LT.lt.ne', Fact.out, HMul.hMul, Membership.mem, Set, Set.Ico, HAdd.hAdd, Equiv and 2 more

    Proof uses: funext, AddCircle.coe_equivIco, Eq.mpr, id, congrArg, Eq.symm, AddCircle.equivAddCircle_apply_mk, Eq.refl

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  9. lemma AddCircle.continuous_equivAddCircle line 76 source

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

    Statement uses: Field, LinearOrder, IsStrictOrderedRing, TopologicalSpace, OrderTopology, Fact, LT.lt, OfNat.ofNat, Continuous, AddCircle, AddSubgroup.zmultiples, AddEquiv, AddCircle.equivAddCircle, LT.lt.ne', Fact.out

    Proof uses: Homeomorph.continuous_toFun, AddCircle.homeomorphAddCircle

    42 instances, coercions and auxiliary constants left out.

  10. lemma AddCircle.measurePreserving_equivAddCircle line 81 source

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

    Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.MeasurePreserving, AddCircle, AddSubgroup.zmultiples, AddEquiv, AddCircle.equivAddCircle, LT.lt.ne', Fact.out, AddCircle.haarAddCircle

    Proof uses: AddMonoidHom.measurePreserving, QuotientAddGroup.map, AddAut.mulRight, HMul.hMul, Units, Inv.inv, Units.mk0, AddCircle.continuous_equivAddCircle, AddEquiv.surjective, of_eq_true, Eq, ENNReal, MeasureTheory.Measure, Set, Set.univ, Eq.trans, True, congr, congrArg, MeasureTheory.IsProbabilityMeasure.measure_univ and 1 more

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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