ProperSpace

📁 Source: Mathlib/Analysis/Normed/Field/ProperSpace.lean

Statistics

Metric	Count
Definitions	0
Theorems of_nontriviallyNormedField_of_weaklyLocallyCompactSpace	1
Total	1

ProperSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_nontriviallyNormedField_of_weaklyLocallyCompactSpace 📖	mathematical	—	ProperSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	Metric.exists_isCompact_closedBall NormedField.exists_one_lt_norm pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass norm_zero LE.le.not_gt zero_le_one Real.instZeroLEOneClass Set.ext dist_zero_right Set.mem_smul_set_iff_inv_smul_mem₀ norm_mul norm_inv norm_pow NormedDivisionRing.to_normOneClass inv_mul_le_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff IsCompact.smul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Filter.Tendsto.atTop_mul_const tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean of_seq_closedBall Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.of_forall

---

← Back to Index