SubmonoidClosure

📁 Source: Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean

Statistics

Metric	Count
Definitions	0
Theorems closure_addSubmonoidClosure_eq_closure_addSubgroupClosure, closure_range_zpow_eq_pow, closure_range_zsmul_eq_nsmul, closure_submonoidClosure_eq_closure_subgroupClosure, denseRange_zpow_iff_pow, denseRange_zsmul_iff_nsmul, dense_addSubmonoidClosure_iff_addSubgroupClosure, dense_submonoidClosure_iff_subgroupClosure, mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples, mapClusterPt_atTop_nsmul_tfae, mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, mapClusterPt_atTop_pow_tfae, mapClusterPt_atTop_zpow_iff_pow, mapClusterPt_atTop_zsmul_iff_nsmul, mapClusterPt_inv_atTop_pow, mapClusterPt_neg_atTop_nsmul, mapClusterPt_one_atTop_pow, mapClusterPt_self_atTop_nsmul, mapClusterPt_self_atTop_pow, mapClusterPt_self_zpow_atTop_pow, mapClusterPt_self_zsmul_atTop_nsmul, mapClusterPt_zero_atTop_nsmul, topologicalClosure_addSubgroupClosure_toAddSubmonoid, topologicalClosure_subgroupClosure_toSubmonoid	24
Total	24

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_addSubmonoidClosure_eq_closure_addSubgroupClosure 📖	mathematical	—	closure SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubmonoid.instSetLike AddSubmonoid.closure AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure	—	IsTopologicalAddGroup.toContinuousAdd topologicalClosure_addSubgroupClosure_toAddSubmonoid
closure_range_zpow_eq_pow 📖	mathematical	—	closure Set.range DivInvMonoid.toZPow Group.toDivInvMonoid Monoid.toNatPow DivInvMonoid.toMonoid	—	Set.ext List.TFAE.out mapClusterPt_atTop_pow_tfae
closure_range_zsmul_eq_nsmul 📖	mathematical	—	closure Set.range SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	Set.ext List.TFAE.out mapClusterPt_atTop_nsmul_tfae
closure_submonoidClosure_eq_closure_subgroupClosure 📖	mathematical	—	closure SetLike.coe Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Submonoid.instSetLike Submonoid.closure Subgroup Subgroup.instSetLike Subgroup.closure	—	IsTopologicalGroup.toContinuousMul topologicalClosure_subgroupClosure_toSubmonoid
denseRange_zpow_iff_pow 📖	mathematical	—	DenseRange DivInvMonoid.toZPow Group.toDivInvMonoid Monoid.toNatPow DivInvMonoid.toMonoid	—	closure_range_zpow_eq_pow
denseRange_zsmul_iff_nsmul 📖	mathematical	—	DenseRange SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	dense_iff_closure_eq closure_range_zsmul_eq_nsmul
dense_addSubmonoidClosure_iff_addSubgroupClosure 📖	mathematical	—	Dense SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubmonoid.instSetLike AddSubmonoid.closure AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure	—	dense_iff_closure_eq closure_addSubmonoidClosure_eq_closure_addSubgroupClosure
dense_submonoidClosure_iff_subgroupClosure 📖	mathematical	—	Dense SetLike.coe Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Submonoid.instSetLike Submonoid.closure Subgroup Subgroup.instSetLike Subgroup.closure	—	closure_submonoidClosure_eq_closure_subgroupClosure
mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples 📖	mathematical	—	MapClusterPt Filter.atTop Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.topologicalClosure AddSubgroup.zmultiples	—	List.TFAE.out mapClusterPt_atTop_nsmul_tfae
mapClusterPt_atTop_nsmul_tfae 📖	mathematical	—	List.TFAE MapClusterPt Filter.atTop Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt SubNegMonoid.toZSMul Set Set.instMembership closure Set.range	—	mapClusterPt_atTop_zsmul_iff_nsmul closure_mono Set.range_subset_iff natCast_zsmul closure_minimal mapClusterPt_self_zsmul_atTop_nsmul isClosed_setOf_clusterPt mem_closure_iff_clusterPt ClusterPt.mono Filter.le_principal_iff Filter.range_mem_map List.tfae_of_cycle
mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers 📖	mathematical	—	MapClusterPt Filter.atTop Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.topologicalClosure Subgroup.zpowers	—	List.TFAE.out mapClusterPt_atTop_pow_tfae
mapClusterPt_atTop_pow_tfae 📖	mathematical	—	List.TFAE MapClusterPt Filter.atTop Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DivInvMonoid.toZPow Set Set.instMembership closure Set.range	—	mapClusterPt_atTop_zpow_iff_pow closure_mono Set.range_subset_iff zpow_natCast closure_minimal mapClusterPt_self_zpow_atTop_pow isClosed_setOf_clusterPt mem_closure_iff_clusterPt ClusterPt.mono Filter.le_principal_iff Filter.range_mem_map List.tfae_of_cycle
mapClusterPt_atTop_zpow_iff_pow 📖	mathematical	—	MapClusterPt Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DivInvMonoid.toZPow Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid	—	Filter.map_map zpow_natCast
mapClusterPt_atTop_zsmul_iff_nsmul 📖	mathematical	—	MapClusterPt Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt SubNegMonoid.toZSMul Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	Nat.map_cast_int_atTop Filter.map_map natCast_zsmul
mapClusterPt_inv_atTop_pow 📖	mathematical	—	MapClusterPt InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Filter.atTop Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	SubgroupClass.toInvMemClass Subgroup.instSubgroupClass
mapClusterPt_neg_atTop_nsmul 📖	mathematical	—	MapClusterPt NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Filter.atTop Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples neg_mem_iff AddSubgroupClass.toNegMemClass AddSubgroup.instAddSubgroupClass
mapClusterPt_one_atTop_pow 📖	mathematical	—	MapClusterPt InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Filter.atTop Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	zpow_zero mapClusterPt_self_zpow_atTop_pow
mapClusterPt_self_atTop_nsmul 📖	mathematical	—	MapClusterPt Filter.atTop Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	one_zsmul mapClusterPt_self_zsmul_atTop_nsmul
mapClusterPt_self_atTop_pow 📖	mathematical	—	MapClusterPt Filter.atTop Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	zpow_one mapClusterPt_self_zpow_atTop_pow
mapClusterPt_self_zpow_atTop_pow 📖	mathematical	—	MapClusterPt DivInvMonoid.toZPow Group.toDivInvMonoid Filter.atTop Nat.instPreorder Monoid.toNatPow DivInvMonoid.toMonoid	—	exists_clusterPt_of_compactSpace Filter.map_neBot Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing instArchimedeanInt mapClusterPt_atTop_zpow_iff_pow ContinuousAt.div' IsTopologicalGroup.to_continuousDiv ContinuousAt.fun_mul IsTopologicalGroup.toContinuousMul continuousAt_const ContinuousAt.snd continuousAt_id' ContinuousAt.fst div_eq_mul_inv mul_inv_cancel_right MapClusterPt.continuousAt_comp MapClusterPt.curry_prodMap Filter.Tendsto.curry Filter.Eventually.of_forall sub_eq_add_neg Filter.tendsto_atTop_add_const_right Int.instIsOrderedAddMonoid Filter.tendsto_atTop_add_const_left Filter.tendsto_id MapClusterPt.of_comp
mapClusterPt_self_zsmul_atTop_nsmul 📖	mathematical	—	MapClusterPt SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Filter.atTop Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	exists_clusterPt_of_compactSpace Filter.map_neBot Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing instArchimedeanInt mapClusterPt_atTop_zsmul_iff_nsmul ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub ContinuousAt.fun_add IsTopologicalAddGroup.toContinuousAdd continuousAt_const ContinuousAt.snd continuousAt_id' ContinuousAt.fst sub_eq_add_neg add_neg_cancel_right add_zsmul sub_zsmul MapClusterPt.continuousAt_comp MapClusterPt.curry_prodMap Filter.Tendsto.curry Filter.Eventually.of_forall Filter.tendsto_atTop_add_const_right Int.instIsOrderedAddMonoid Filter.tendsto_atTop_add_const_left Filter.tendsto_id MapClusterPt.of_comp
mapClusterPt_zero_atTop_nsmul 📖	mathematical	—	MapClusterPt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Filter.atTop Nat.instPreorder AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	zero_zsmul mapClusterPt_self_zsmul_atTop_nsmul
topologicalClosure_addSubgroupClosure_toAddSubmonoid 📖	mathematical	—	AddSubmonoid.topologicalClosure SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid IsTopologicalAddGroup.toContinuousAdd AddSubgroup.toAddSubmonoid AddSubgroup.closure AddSubmonoid.closure AddMonoid.toAddZeroClass	—	le_antisymm IsTopologicalAddGroup.toContinuousAdd AddSubmonoid.topologicalClosure_minimal AddSubgroup.closure_toAddSubmonoid AddSubmonoid.closure_le Set.union_subset HasSubset.Subset.trans Set.instIsTransSubset AddSubmonoid.subset_closure subset_closure closure_mono AddSubmonoid.multiples_le Set.mem_neg AddSubmonoid.coe_multiples closure_range_zsmul_eq_nsmul AddSubgroup.coe_zmultiples AddSubgroup.topologicalClosure_coe SetLike.mem_coe neg_mem_iff AddSubgroupClass.toNegMemClass AddSubgroup.instAddSubgroupClass AddSubgroup.mem_zmultiples isClosed_closure AddSubgroup.le_closure_toAddSubmonoid
topologicalClosure_subgroupClosure_toSubmonoid 📖	mathematical	—	Submonoid.topologicalClosure DivInvMonoid.toMonoid Group.toDivInvMonoid IsTopologicalGroup.toContinuousMul Subgroup.toSubmonoid Subgroup.closure Submonoid.closure Monoid.toMulOneClass	—	le_antisymm IsTopologicalGroup.toContinuousMul Submonoid.topologicalClosure_minimal Subgroup.closure_toSubmonoid Submonoid.closure_le Set.union_subset HasSubset.Subset.trans Set.instIsTransSubset Submonoid.subset_closure subset_closure closure_mono Submonoid.powers_le Set.mem_inv Submonoid.coe_powers closure_range_zpow_eq_pow Subgroup.coe_zpowers Subgroup.topologicalClosure_coe SetLike.mem_coe inv_mem_iff SubgroupClass.toInvMemClass Subgroup.instSubgroupClass Subgroup.mem_zpowers isClosed_closure Subgroup.le_closure_toSubmonoid

---

← Back to Index