Documentation Verification Report

SeparatedNhds

📁 Source: Mathlib/Topology/Separation/SeparatedNhds.lean

Statistics

Metric	Count
Definitions `HasSeparatingCover`, `SeparatedNhds`	2
Theorems `mono`, `comm`, `disjoint`, `disjoint_closure_left`, `disjoint_closure_right`, `disjoint_nhdsSet`, `empty_left`, `empty_right`, `isClosed_left_of_isClosed_union`, `isClosed_right_of_isClosed_union`, `isClosed_union_iff`, `isOpen_left_of_isOpen_union`, `isOpen_right_of_isOpen_union`, `isOpen_union_iff`, `mono`, `preimage`, `union_left`, `union_right`, `hasSeparatingCover_empty_left`, `hasSeparatingCover_empty_right`, `hasSeparatingCovers_iff_separatedNhds`, `separatedNhds_iff_disjoint`	22
Total	24

HasSeparatingCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`HasSeparatingCover` `Set` `Set.instHasSubset`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.disjoint_of_subset`

SeparatedNhds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`SeparatedNhds`	—	`symm`
`disjoint` 📖	mathematical	`SeparatedNhds`	`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`	—	`Disjoint.mono`
`disjoint_closure_left` 📖	mathematical	`SeparatedNhds`	`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` `closure`	—	`Disjoint.mono` `closure_mono` `Disjoint.closure_left`
`disjoint_closure_right` 📖	mathematical	`SeparatedNhds`	`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` `closure`	—	`Disjoint.symm` `disjoint_closure_left` `symm`
`disjoint_nhdsSet` 📖	mathematical	`SeparatedNhds`	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet`	—	`separatedNhds_iff_disjoint`
`empty_left` 📖	mathematical	—	`SeparatedNhds` `Set` `Set.instEmptyCollection`	—	`symm` `empty_right`
`empty_right` 📖	mathematical	—	`SeparatedNhds` `Set` `Set.instEmptyCollection`	—	`isOpen_univ` `isOpen_empty` `Set.mem_univ` `Set.Subset.rfl` `Set.disjoint_empty`
`isClosed_left_of_isClosed_union` 📖	mathematical	`SeparatedNhds`	`IsClosed`	—	`isOpen_compl_iff` `compl_inj_iff` `Set.compl_union` `compl_compl` `Set.union_inter_distrib_right` `Disjoint.inter_eq` `Disjoint.mono_left` `disjoint_compl_right` `Set.union_empty` `Set.left_eq_inter` `Set.subset_compl_comm` `Disjoint.subset_compl_left` `IsOpen.union`
`isClosed_right_of_isClosed_union` 📖	mathematical	`SeparatedNhds`	`IsClosed`	—	`isClosed_left_of_isClosed_union` `symm` `Set.union_comm`
`isClosed_union_iff` 📖	mathematical	`SeparatedNhds`	`IsClosed` `Set` `Set.instUnion`	—	`isClosed_left_of_isClosed_union` `isClosed_right_of_isClosed_union` `IsClosed.union`
`isOpen_left_of_isOpen_union` 📖	—	`SeparatedNhds` `IsOpen` `Set` `Set.instUnion`	—	—	`Set.union_inter_distrib_right` `Disjoint.inter_eq` `Disjoint.mono_left` `Disjoint.symm` `Set.union_empty` `Set.inter_eq_left` `IsOpen.inter`
`isOpen_right_of_isOpen_union` 📖	—	`SeparatedNhds` `IsOpen` `Set` `Set.instUnion`	—	—	`isOpen_left_of_isOpen_union` `symm` `Set.union_comm`
`isOpen_union_iff` 📖	mathematical	`SeparatedNhds`	`IsOpen` `Set` `Set.instUnion`	—	`isOpen_left_of_isOpen_union` `isOpen_right_of_isOpen_union` `IsOpen.union`
`mono` 📖	—	`SeparatedNhds` `Set` `Set.instHasSubset`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`
`preimage` 📖	mathematical	`SeparatedNhds` `Continuous`	`Set.preimage`	—	`IsOpen.preimage` `Set.preimage_mono` `Disjoint.preimage`
`union_left` 📖	mathematical	`SeparatedNhds`	`Set` `Set.instUnion`	—	`nhdsSet_union`
`union_right` 📖	mathematical	`SeparatedNhds`	`Set` `Set.instUnion`	—	`symm` `union_left`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSeparatingCover_empty_left` 📖	mathematical	—	`HasSeparatingCover` `Set` `instEmptyCollection`	—	`empty_subset` `isOpen_empty` `closure_empty`
`hasSeparatingCover_empty_right` 📖	mathematical	—	`HasSeparatingCover` `Set` `instEmptyCollection`	—	`HasSubset.Subset.trans` `instIsTransSubset` `subset_univ` `Eq.subset` `instReflSubset` `iUnion_const` `isOpen_univ` `disjoint_empty`

(root)

Definitions

Name	Category	Theorems
`HasSeparatingCover` 📖	MathDef	5 math math: `Set.hasSeparatingCover_empty_left`, `hasSeparatingCovers_iff_separatedNhds`, `Disjoint.hasSeparatingCover_closed_gdelta_right`, `IsClosed.HasSeparatingCover`, `Set.hasSeparatingCover_empty_right`
`SeparatedNhds` 📖	MathDef	13 math math: `SeparatedNhds.of_isCompact_isClosed`, `SeparatedNhds.comm`, `normal_separation`, `SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed`, `SeparatedNhds.of_finset_finset`, `hasSeparatingCovers_iff_separatedNhds`, `separatedNhds_iff_disjoint`, `NormalSpace.normal`, `SeparatedNhds.empty_right`, `SeparatedNhds.of_isCompact_isCompact_isClosed`, `SeparatedNhds.empty_left`, `SeparatedNhds.of_isCompact_isCompact`, `SeparatedNhds.of_singleton_finset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSeparatingCovers_iff_separatedNhds` 📖	mathematical	—	`HasSeparatingCover` `SeparatedNhds`	—	`isOpen_iUnion` `IsOpen.sdiff` `isClosed_closure` `closure_iUnion₂_le_nat` `Set.disjoint_left` `subset_closure` `Set.mem_biUnion` `le_of_lt` `not_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `Set.iUnion_const` `Set.disjoint_of_subset` `Disjoint.closure_left` `Disjoint.symm` `Disjoint.closure_right`
`separatedNhds_iff_disjoint` 📖	mathematical	—	`SeparatedNhds` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet`	—	`Filter.HasBasis.disjoint_iff` `hasBasis_nhdsSet`

---

← Back to Index