Documentation Verification Report

TotallyDisconnected

📁 Source: Mathlib/Topology/Algebra/Nonarchimedean/TotallyDisconnected.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_openAddSubgroup_separating`, `instTotallySeparated`, `exists_openSubgroup_separating`, `instTotallySeparated`	4
Total	4

NonarchimedeanAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_openAddSubgroup_separating` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `OpenAddSubgroup` `OpenAddSubgroup.instSetLike`	—	`t2_separation` `neg_add_eq_zero` `is_nonarchimedean` `IsOpen.mem_nhds` `Set.subset_empty_iff` `Set.nonempty_iff_ne_empty` `Disjoint.subset_compl_right` `SetLike.mem_coe` `neg_add_rev` `neg_neg` `add_assoc` `add_neg_cancel_left` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `OpenAddSubgroup.instAddSubgroupClass` `mem_leftAddCoset_iff` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass`
`instTotallySeparated` 📖	mathematical	—	`TotallySeparatedSpace`	—	`exists_openAddSubgroup_separating` `IsOpen.vadd` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `IsTopologicalAddGroup.toContinuousAdd` `toIsTopologicalAddGroup` `OpenAddSubgroup.isOpen` `IsClosed.isOpen_compl` `IsClosed.vadd` `OpenAddSubgroup.isClosed` `mem_own_leftAddCoset` `Disjoint.subset_compl_left` `Set.union_compl_self` `subset_refl` `Set.instReflSubset` `disjoint_compl_right`

NonarchimedeanGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_openSubgroup_separating` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `OpenSubgroup` `OpenSubgroup.instSetLike`	—	`t2_separation` `inv_mul_eq_one` `is_nonarchimedean` `IsOpen.mem_nhds` `Disjoint.subset_compl_right` `mul_inv_rev` `inv_inv` `mul_assoc` `mul_inv_cancel_left` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `OpenSubgroup.instSubgroupClass` `mem_leftCoset_iff` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass`
`instTotallySeparated` 📖	mathematical	—	`TotallySeparatedSpace`	—	`exists_openSubgroup_separating` `IsOpen.smul` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `IsTopologicalGroup.toContinuousMul` `toIsTopologicalGroup` `OpenSubgroup.isOpen` `IsClosed.isOpen_compl` `IsClosed.smul` `OpenSubgroup.isClosed` `mem_own_leftCoset` `Disjoint.subset_compl_left` `Set.union_compl_self` `Set.instReflSubset` `disjoint_compl_right`

---

← Back to Index