FLT/Mathlib/Topology/HomToDiscrete.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem DiscretePi line 18 source

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

   Statement uses: TopologicalSpace, Nat, Exists, Set, And, IsOpen, Eq, Set.preimage, Singleton.singleton, Fin

   Proof uses: Exists.intro, Set.pi, Set.univ, Classical.choose, And.intro, isOpen_set_pi, Set.finite_univ, Membership.mem, And.left, Classical.choose_spec, Set.ext, Eq.mpr, Iff, id, congr, congrArg, Eq.trans, forall_congr, True, implies_congr and 12 more

   14 instances, coercions and auxiliary constants left out.

   Tactic trace: 18 steps

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

2. theorem HomeoDiscrete_of_Discrete line 38 source

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

   Statement uses: TopologicalSpace, Homeomorph, Exists, Set, And, IsOpen, Eq, Set.preimage, Singleton.singleton, Function.comp

   Proof uses: Exists.intro, Set.image, And.intro, Iff.mpr, Homeomorph.isOpen_image, Set.ext, Eq.mpr, Iff, Membership.mem, id, congr, congrArg, Eq.trans, funext, Iff.intro, Eq.mp, congrFun', of_eq_true, True, eq_self

   19 instances, coercions and auxiliary constants left out.

   Tactic trace: 12 steps

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

3. theorem Discrete_of_HomeoDiscrete line 53 source

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

   Statement uses: TopologicalSpace, Homeomorph, Exists, Set, And, IsOpen, Eq, Set.preimage, Function.comp, Singleton.singleton

   Proof uses: Exists.intro, Set.image, Homeomorph.symm, And.intro, Iff.mpr, Homeomorph.isOpen_image, Set.ext, Eq.mpr, Iff, Membership.mem, id, congr, congrArg, Eq.trans, Iff.intro, Eq.symm, Homeomorph.apply_symm_apply, Eq.mp, congrFun', of_eq_true and 3 more

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 17 steps

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

4. theorem HomeoDiscrete_iff_Discrete line 70 source

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

   Statement uses: TopologicalSpace, Homeomorph, Iff, Exists, Set, And, IsOpen, Eq, Set.preimage, Singleton.singleton, Function.comp

   Proof uses: Iff.intro, HomeoDiscrete_of_Discrete, Discrete_of_HomeoDiscrete

   8 instances, coercions and auxiliary constants left out.

5. theorem HomDiscrete_of_Discrete line 76 source

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

   Statement uses: TopologicalSpace, Equiv, Exists, Set, And, IsOpen, Eq, Set.preimage, Singleton.singleton, Set.image

   Proof uses: Equiv.symm, Exists.intro, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, Set.image_singleton, Equiv.apply_symm_apply, eq_self

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

6. theorem Discrete_of_HomDiscrete line 82 source

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

   Statement uses: TopologicalSpace, Equiv, Exists, Set, And, IsOpen, Eq, Set.image, Set.preimage, Singleton.singleton

   Proof uses: Exists.intro, And.intro, Eq.mpr, id, congrFun', congrArg, Iff.mpr, Equiv.eq_preimage_iff_image_eq, of_eq_true, Eq.trans, True, Set.image_singleton, eq_self

   11 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

7. theorem HomDiscrete_iff_Discrete line 90 source

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

   Statement uses: TopologicalSpace, Equiv, Iff, Exists, Set, And, IsOpen, Eq, Set.image, Set.preimage, Singleton.singleton

   Proof uses: Iff.intro, Discrete_of_HomDiscrete, HomDiscrete_of_Discrete

   8 instances, coercions and auxiliary constants left out.

8. lemma inter_Discrete line 99 source

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

   Statement uses: TopologicalSpace, Set, DiscreteTopology, Membership.mem, Inter.inter

   Proof uses: Iff.mpr, IsOpen, Singleton.singleton, discreteTopology_iff_isOpen_singleton, TopologicalSpace.mk, Subtype, Exists, And, Eq, Set.preimage, Subtype.mk, And.intro, isOpen_mk, inferInstance, Iff.mp, Exists.intro, Eq.mp, congr, congrArg, Eq.trans and 17 more

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 9 steps

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

9. lemma Discrete_inter line 111 source

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

   Statement uses: TopologicalSpace, Set, DiscreteTopology, Membership.mem, Inter.inter

   Proof uses: Eq.mpr, id, Eq, congrArg, Set.inter_comm, inter_Discrete

   8 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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