Documentation Verification Report

Topology

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

Statistics

Metric	Count
Definitions	0
Theorems `isAdicComplete_iff`, `isHausdorff_iff`, `isPrecomplete_iff`, `congr_ringEquiv`, `congr_ringEquiv`, `congr_ringEquiv`	6
Total	6

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` `UniformSpace.toTopologicalSpace`	—	`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` `instReflLe` `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`

IsAdicComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_ringEquiv` 📖	mathematical	—	`IsAdicComplete` `Ideal.map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	—

IsHausdorff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_ringEquiv` 📖	mathematical	—	`IsHausdorff` `Ideal.map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	`IsAdic.isHausdorff_iff` `Homeomorph.t2Space`

IsPrecomplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_ringEquiv` 📖	mathematical	—	`IsPrecomplete` `Ideal.map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	`IsAdic.isPrecomplete_iff` `WithIdeal.instIsUniformAddGroup` `completeSpace_congr` `UniformEquiv.isUniformEmbedding`

---

← Back to Index