Topology

📁 Source: Mathlib/RingTheory/AdicCompletion/Topology.lean

Statistics

Metric	Count
Definitions	0
Theorems isAdicComplete_iff, isHausdorff_iff, isPrecomplete_iff	3
Total	3

IsAdic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAdicComplete_iff 📖	mathematical	IsAdic UniformSpace.toTopologicalSpace	IsAdicComplete Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring CompleteSpace T2Space	—	isAdicComplete_iff isHausdorff_iff isPrecomplete_iff
isHausdorff_iff 📖	mathematical	IsAdic	IsHausdorff Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring T2Space	—	AddGroupFilterBasis.t2Space_iff_sInter_subset IsScalarTower.left IsScalarTower.right isHausdorff_iff Ideal.mul_top Ideal.instIsTwoSided_1
isPrecomplete_iff 📖	mathematical	IsAdic UniformSpace.toTopologicalSpace	IsPrecomplete Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring CompleteSpace	—	Filter.HasBasis.isCountablyGenerated instCountableNat hasBasis_nhds_zero IsUniformAddGroup.uniformity_countably_generated IsScalarTower.right IsScalarTower.left Ideal.mul_top Ideal.instIsTwoSided_1 UniformSpace.complete_of_cauchySeq_tendsto Filter.HasBasis.cauchySeq_iff Filter.HasBasis.uniformity_of_nhds_zero Finset.le_sup Ideal.add_mem LE.le.trans sub_add_sub_cancel Filter.HasBasis.tendsto_right_iff hasBasis_nhds Set.image_add_left instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat sub_eq_neg_add CompleteSpace.complete sub_sub_sub_cancel_left Ideal.sub_mem sub_add_sub_cancel' le_sup_right le_max_left

---

← Back to Index