Documentation Verification Report

T5

📁 Source: Mathlib/Topology/Order/T5.lean

Statistics

Metric	Count
Definitions	0
Theorems `completelyNormalSpace`, `t5Space`, `compl_ordConnectedSection_ordSeparatingSet_mem_nhds`, `compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE`, `compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE`, `ordConnectedComponent_mem_nhds`, `ordT5Nhd_mem_nhdsSet`	7
Total	7

OrderTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completelyNormalSpace` 📖	mathematical	—	`CompletelyNormalSpace`	—	`Filter.disjoint_iff` `Set.ordT5Nhd_mem_nhdsSet` `Disjoint.symm` `Set.disjoint_ordT5Nhd`
`t5Space` 📖	mathematical	—	`T5Space`	—	`T2Space.t1Space` `OrderClosedTopology.to_t2Space` `to_orderClosedTopology` `completelyNormalSpace`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_ordConnectedSection_ordSeparatingSet_mem_nhds` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure` `instMembership`	`Filter` `Filter.instMembership` `nhds` `Compl.compl` `instCompl` `ordConnectedSection` `ordSeparatingSet`	—	`nhdsLE_sup_nhdsGE` `Filter.mem_sup` `compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE` `compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE`
`compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure` `instMembership`	`Filter` `Filter.instMembership` `nhdsWithin` `Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Compl.compl` `instCompl` `ordConnectedSection` `ordSeparatingSet`	—	`mem_nhdsWithin_of_mem_nhds` `mem_interior_iff_mem_nhds` `interior_compl` `disjoint_left` `exists_Icc_mem_subset_of_mem_nhdsGE` `Filter.mem_of_superset` `subset_ordConnectedComponent` `ordConnected_Icc` `left_mem_Icc` `Disjoint.mono_right` `ordConnectedSection_subset` `disjoint_left_ordSeparatingSet` `LE.le.lt_of_ne` `Filter.mp_mem` `Ico_mem_nhdsGE` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Filter.univ_mem'` `LT.lt.ne` `eq_of_mem_ordConnectedSection_of_uIcc_subset` `subset_inter` `subset_iUnion₂_of_subset` `OrdConnected.uIcc_subset` `instOrdConnectedOrdConnectedComponent` `LE.le.trans` `LT.lt.le` `mem_iUnion₂` `ordConnected_uIcc` `left_mem_uIcc` `lt_of_not_ge` `not_le` `Icc_subset_uIcc` `uIcc_of_ge` `LT.lt.trans`
`compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure` `instMembership`	`Filter` `Filter.instMembership` `nhdsWithin` `Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Compl.compl` `instCompl` `ordConnectedSection` `ordSeparatingSet`	—	`dual_ordSeparatingSet` `dual_ordConnectedSection` `compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE` `instOrderTopologyOrderDual`
`ordConnectedComponent_mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `ordConnectedComponent`	—	`Filter.mem_of_superset` `ordConnectedComponent_subset` `exists_Icc_mem_subset_of_mem_nhds` `subset_ordConnectedComponent` `ordConnected_Icc`
`ordT5Nhd_mem_nhdsSet` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure`	`Filter` `Filter.instMembership` `nhdsSet` `ordT5Nhd`	—	`bUnion_mem_nhdsSet` `ordConnectedComponent_mem_nhds` `Filter.inter_mem` `mem_interior_iff_mem_nhds` `interior_compl` `disjoint_left` `compl_ordConnectedSection_ordSeparatingSet_mem_nhds`

---

← Back to Index