ArchimedeanDiscrete

📁 Source: Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean

Statistics

Metric	Count
Definitions	0
Theorems discrete_iff_addCyclic, instDiscreteTopologyZMultiples, instIsAddCyclicOfDiscreteTopology, discrete_iff_cyclic, instDiscreteTopologyZMultiples, instIsCyclicOfDiscreteTopology	6
Total	6

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrete_iff_addCyclic 📖	mathematical	—	IsAddCyclic AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike zsmul DiscreteTopology instTopologicalSpaceSubtype	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim isAddCyclic_of_subsingleton instSubsingletonSubtype_mathlib Subsingleton.discreteTopology isAddCyclic_iff_exists_zmultiples_eq_top instDiscreteTopologyZMultiples dense_or_cyclic zmultiples_eq_closure Homeomorph.discreteTopology_iff isAddCyclic_iff_exists_zmultiples_eq_top instIsAddCyclicOfDiscreteTopology coe_eq_univ dense_iff_closure_eq IsClosed.closure_eq isClosed_of_discrete LinearOrderedAddCommGroup.toIsTopologicalAddGroup OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology
instDiscreteTopologyZMultiples 📖	mathematical	—	DiscreteTopology AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike zmultiples instTopologicalSpaceSubtype	—	eq_or_lt_of_le zmultiples_zero_eq_bot Subsingleton.discreteTopology Unique.instSubsingleton discreteTopology_iff_isOpen_singleton_zero IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroupSubtypeMem LinearOrderedAddCommGroup.toIsTopologicalAddGroup isOpen_induced_iff isOpen_Ioo OrderTopology.to_orderClosedTopology Set.ext Set.mem_preimage Set.mem_Ioo Set.mem_singleton_iff zsmul_lt_zsmul_iff_left zero_zsmul neg_zsmul one_zsmul Left.neg_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono zmultiples_neg neg_nonneg le_of_not_ge
instIsAddCyclicOfDiscreteTopology 📖	mathematical	—	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim isAddCyclic_of_subsingleton LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered DenselyOrdered.subsingleton_of_discreteTopology false_of_nontrivial_of_subsingleton

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrete_iff_cyclic 📖	mathematical	—	IsCyclic Subgroup CommGroup.toGroup SetLike.instMembership instSetLike zpow DiscreteTopology instTopologicalSpaceSubtype	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim instSubsingletonSubtype_mathlib isCyclic_iff_exists_zpowers_eq_top instDiscreteTopologyZMultiples dense_or_cyclic Homeomorph.discreteTopology_iff isCyclic_iff_exists_zpowers_eq_top instIsCyclicOfDiscreteTopology coe_eq_univ dense_iff_closure_eq IsClosed.closure_eq isClosed_of_discrete LinearOrderedCommGroup.toIsTopologicalGroup OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology
instDiscreteTopologyZMultiples 📖	mathematical	—	DiscreteTopology Subgroup CommGroup.toGroup SetLike.instMembership instSetLike zpowers instTopologicalSpaceSubtype	—	eq_or_lt_of_le zpowers_one_eq_bot Subsingleton.discreteTopology Unique.instSubsingleton discreteTopology_iff_isOpen_singleton_one IsTopologicalGroup.toContinuousMul instIsTopologicalGroupSubtypeMem LinearOrderedCommGroup.toIsTopologicalGroup isOpen_induced_iff isOpen_Ioo OrderTopology.to_orderClosedTopology Set.ext zpow_lt_zpow_iff_right zpow_zero zpow_neg zpow_one IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono zpowers_inv one_le_inv' le_of_not_ge
instIsCyclicOfDiscreteTopology 📖	mathematical	—	IsCyclic DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim isCyclic_of_subsingleton LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered DenselyOrdered.subsingleton_of_discreteTopology false_of_nontrivial_of_subsingleton

---

← Back to Index