ProperSpace

📁 Source: Mathlib/NumberTheory/Padics/ProperSpace.lean

Statistics

Metric	Count
Definitions	0
Theorems instProperSpace, compactSpace, totallyBounded_univ	3
Total	3

Padic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instProperSpace 📖	mathematical	—	ProperSpace Padic SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing normedField	—	Metric.closedBall_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup SeminormedAddCommGroup.toIsTopologicalAddGroup PadicInt.compactSpace dist_eq_norm_sub sub_zero ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace

PadicInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace PadicInt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNormedCommRing	—	isCompact_univ_iff isCompact_iff_totallyBounded_isComplete totallyBounded_univ complete_univ completeSpace
totallyBounded_univ 📖	mathematical	—	TotallyBounded PadicInt PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNormedCommRing Set.univ	—	Metric.totallyBounded_iff exists_pow_neg_lt Set.toFinite Finite.Set.finite_image Finite.of_fintype Set.iUnion_congr_Prop Set.image_congr appr_lt LE.le.trans_lt norm_le_pow_iff_mem_span_pow appr_spec

---

← Back to Index