ZMultiples

📁 Source: Mathlib/Topology/Instances/ZMultiples.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_zmultiples_subtype_cofinite, instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples, tendsto_coe_cofinite, tendsto_zmultiplesHom_cofinite	4
Total	4

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_zmultiples_subtype_cofinite 📖	mathematical	—	Filter.Tendsto Real AddSubgroup Real.instAddGroup SetLike.instMembership instSetLike zmultiples DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddMonoidHom.instFunLike subtype Filter.cofinite Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	tendsto_coe_cofinite_of_discrete instIsTopologicalAddGroupReal TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity SetLike.isDiscrete_iff_discreteTopology Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples 📖	mathematical	—	DiscreteTopology Real AddSubgroup Real.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	eq_or_ne AddSubgroup.zmultiples_zero_eq_bot Subsingleton.discreteTopology Unique.instSubsingleton discreteTopology_iff_isOpen_singleton_zero IsTopologicalAddGroup.toContinuousAdd AddSubgroup.instIsTopologicalAddGroupSubtypeMem instIsTopologicalAddGroupReal isOpen_induced_iff Metric.isOpen_ball Set.ext AddSubgroup.mem_zmultiples_iff zsmul_eq_mul sub_zero abs_mul Real.instIsOrderedRing IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one cast_one Real.instZeroLEOneClass NeZero.one Real.instNontrivial IsStrictOrderedRing.noZeroDivisors AddGroup.existsAddOfLE IsStrictOrderedRing.toCharZero
tendsto_coe_cofinite 📖	mathematical	—	Filter.Tendsto Real Real.instIntCast Filter.cofinite Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	AddMonoidHom.tendsto_coe_cofinite_of_discrete instIsTopologicalAddGroupReal TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity cast_injective IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing range_castAddHom SetLike.isDiscrete_iff_discreteTopology instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples
tendsto_zmultiplesHom_cofinite 📖	mathematical	—	Filter.Tendsto Real DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instAddGroup AddMonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike zmultiplesHom Filter.cofinite Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	AddMonoidHom.tendsto_coe_cofinite_of_discrete instIsTopologicalAddGroupReal TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity smul_left_injective instIsCancelMulZero instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add AddSubgroup.range_zmultiplesHom SetLike.isDiscrete_iff_discreteTopology instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples

---

← Back to Index