PerfectSpace

📁 Source: Mathlib/Topology/Algebra/Module/PerfectSpace.lean

Statistics

Metric	Count
Definitions PerfectSpace	1
Theorems instPerfectSpace, perfectSpace_of_module	2
Total	3

(root)

Definitions

Name	Category	Theorems
PerfectSpace 📖	CompData	5 math math: perfectSpace_of_module, perfectSpace_def, instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial, perfectSpace_iff_forall_not_isolated, instPerfectSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPerfectSpace 📖	mathematical	—	PerfectSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	perfectSpace_of_module IsSimpleRing.instNontrivial DivisionRing.isSimpleRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul
perfectSpace_of_module 📖	mathematical	—	PerfectSpace	—	NormedField.exists_norm_lt_one exists_ne Filter.Tendsto.add tendsto_const_nhds Filter.Tendsto.smul tendsto_pow_atTop_nhds_zero_of_norm_lt_one zero_smul add_zero AddLeftCancelSemigroup.toIsLeftCancelAdd instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsSimpleRing.instNontrivial DivisionRing.isSimpleRing norm_pos_iff instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat accPt_principal_iff_nhdsWithin Filter.NeBot.mono Filter.NeBot.map Filter.atTop_neBot

---

← Back to Index