Documentation Verification Report

Topology

📁 Source: Mathlib/SetTheory/Ordinal/Topology.lean

Statistics

Metric	Count
Definitions `IsAcc`, `IsClosedBelow`, `instTopologicalSpace`	3
Theorems `forall_lt`, `inter_Ioo_nonempty`, `isSuccLimit`, `mono`, `pos`, `forall_lt`, `iInter`, `sInter`, `accPt_subtype`, `enumOrd_isNormal_iff_isClosed`, `instOrderTopology`, `isAcc_iff`, `isClosedBelow_iff`, `isClosed_iff_bsup`, `isClosed_iff_iSup`, `isOpen_iff`, `isOpen_singleton_iff`, `isSuccLimit_of_mem_frontier`, `mem_closed_iff_bsup`, `mem_closure_iff_bsup`, `mem_closure_iff_iSup`, `mem_closure_tfae`, `mem_iff_iSup_of_isClosed`, `nhds_eq_pure`	24
Total	27

Ordinal

Definitions

Name	Category	Theorems
`IsAcc` 📖	MathDef	2 math math: `isAcc_iff`, `IsAcc.mono`
`IsClosedBelow` 📖	MathDef	3 math math: `isClosedBelow_iff`, `IsClosedBelow.iInter`, `IsClosedBelow.sInter`
`instTopologicalSpace` 📖	CompOp	11 math math: `isOpen_singleton_iff`, `isOpen_iff`, `mem_closure_iff_bsup`, `isClosed_iff_bsup`, `instOrderTopology`, `accPt_subtype`, `mem_closure_iff_iSup`, `mem_closure_tfae`, `enumOrd_isNormal_iff_isClosed`, `isClosed_iff_iSup`, `nhds_eq_pure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accPt_subtype` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`AccPt` `Ordinal` `instTopologicalSpace` `Filter.principal` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.preimage`	—	`Filter.comap_principal` `Topology.IsOpenEmbedding.accPt_comap_iff` `IsOpen.isOpenEmbedding_subtypeVal` `isOpen_Iio` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology`
`enumOrd_isNormal_iff_isClosed` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Order.IsNormal` `Ordinal` `instLinearOrder` `enumOrd` `IsClosed` `instTopologicalSpace`	—	`enumOrd_strictMono` `isClosed_iff_iSup` `Order.IsNormal.map_iSup` `bddAbove_of_small` `small_range` `UnivLE.small` `UnivLE.self` `OrderIso.apply_symm_apply` `enumOrd_mem` `Order.isNormal_iff` `enumOrd_surjective` `isClosed_iff_bsup` `Order.IsSuccLimit.ne_bot` `StrictMono.monotone` `LT.lt.not_ge` `Order.lt_succ` `instNoMaxOrder` `le_bsup` `Order.IsSuccLimit.succ_lt` `LE.le.trans` `bsup_le`
`instOrderTopology` 📖	mathematical	—	`OrderTopology` `Ordinal` `instTopologicalSpace` `PartialOrder.toPreorder` `partialOrder`	—	—
`isAcc_iff` 📖	mathematical	—	`IsAcc` `Set.Nonempty` `Ordinal` `Set` `Set.instInter` `Set.Ioo` `PartialOrder.toPreorder` `partialOrder`	—	`accPt_iff_nhds` `Iio_mem_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `Order.lt_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `Ioo_mem_nhds` `Order.lt_succ` `lt_of_le_of_ne` `Order.lt_succ_iff` `Order.succ_eq_add_one` `exists_Ioc_subset_of_mem_nhds` `pos_iff_ne_zero` `LT.lt.le` `LT.lt.ne`
`isClosedBelow_iff` 📖	mathematical	—	`IsClosedBelow` `Ordinal` `Set` `Set.instMembership`	—	`Topology.IsOpenEmbedding.accPt_comap_iff` `IsOpen.isOpenEmbedding_subtypeVal` `isOpen_Iio` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology`
`isClosed_iff_bsup` 📖	mathematical	—	`IsClosed` `Ordinal` `instTopologicalSpace` `Set` `Set.instMembership` `bsup`	—	`isClosed_iff_iSup` `nonempty_toType_iff` `type_toType` `WellOrderingRel.isWellOrder` `bsup_eq_iSup` `type_ne_zero_iff_nonempty`
`isClosed_iff_iSup` 📖	mathematical	—	`IsClosed` `Ordinal` `instTopologicalSpace` `Set` `Set.instMembership` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`mem_iff_iSup_of_isClosed` `closure_subset_iff_isClosed` `mem_closure_iff_iSup`
`isOpen_iff` 📖	mathematical	—	`IsOpen` `Ordinal` `instTopologicalSpace` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instHasSubset` `Set.Ioo`	—	`SuccOrder.isOpen_iff` `instOrderTopology` `instNoMaxOrder`
`isOpen_singleton_iff` 📖	mathematical	—	`IsOpen` `Ordinal` `instTopologicalSpace` `Set` `Set.instSingletonSet` `Order.IsSuccLimit` `PartialOrder.toPreorder` `partialOrder`	—	`SuccOrder.isOpen_singleton_iff` `instOrderTopology` `instNoMaxOrder`
`isSuccLimit_of_mem_frontier` 📖	mathematical	`Ordinal` `Set` `Set.instMembership` `frontier` `instTopologicalSpace`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	—	`SuccOrder.isSuccLimit_of_mem_frontier` `instOrderTopology` `instNoMaxOrder`
`mem_closed_iff_bsup` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `zero` `bsup`	—	`mem_closure_iff_bsup` `IsClosed.closure_eq`
`mem_closure_iff_bsup` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `closure` `instTopologicalSpace` `zero` `bsup`	—	`List.TFAE.out` `mem_closure_tfae`
`mem_closure_iff_iSup` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `closure` `instTopologicalSpace` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`List.TFAE.out` `mem_closure_tfae`
`mem_closure_tfae` 📖	mathematical	—	`List.TFAE` `Ordinal` `Set` `Set.instMembership` `closure` `instTopologicalSpace` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `partialOrder` `Set.Nonempty` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set.instHasSubset` `BddAbove` `Preorder.toLE` `zero` `bsup` `iSup`	—	`Set.inter_comm` `nhdsWithin_inter'` `SuccOrder.nhdsLE_eq_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `Set.eq_empty_or_nonempty` `IsClosed.closure_eq` `T2Space.t1Space` `OrderClosedTopology.to_t2Space` `IsLUB.csSup_eq` `isLUB_of_mem_closure` `Set.inter_subset_left` `BddAbove.mono` `Set.inter_subset_right` `bddAbove_Iic` `isLUB_csSup` `add_one_ne_zero` `le_antisymm` `bsup_le` `csSup_le` `Eq.trans_le` `le_bsup` `LE.le.trans_lt` `Order.lt_succ` `instNoMaxOrder` `nonempty_toType_iff` `type_toType` `closure_mono` `Set.range_subset_iff` `csSup_mem_closure` `Set.range_nonempty` `bddAbove_range` `List.tfae_of_cycle`
`mem_iff_iSup_of_isClosed` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`mem_closure_iff_iSup` `IsClosed.closure_eq`
`nhds_eq_pure` 📖	mathematical	—	`nhds` `Ordinal` `instTopologicalSpace` `Filter` `Filter.instPure` `Order.IsSuccLimit` `PartialOrder.toPreorder` `partialOrder`	—	`SuccOrder.nhds_eq_pure` `instOrderTopology` `instNoMaxOrder`

Ordinal.IsAcc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Set.Nonempty` `Ordinal` `Set` `Set.instInter` `Set.Ioo` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`Ordinal.isAcc_iff`
`inter_Ioo_nonempty` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Set.Nonempty` `Ordinal` `Set` `Set.instInter` `Set.Ioo` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`forall_lt`
`isSuccLimit` 📖	mathematical	—	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`Ordinal.isSuccLimit_iff` `Ordinal.isAcc_iff` `Order.isSuccPrelimit_of_succ_ne` `lt_of_lt_of_le` `Order.lt_succ` `Ordinal.instNoMaxOrder` `Eq.le` `LE.le.not_gt` `Order.succ_le_iff`
`mono` 📖	mathematical	`Set` `Ordinal` `Set.instHasSubset`	`Ordinal.IsAcc`	—	`Ordinal.isAcc_iff`
`pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.zero`	—	`pos_iff_ne_zero` `Ordinal.canonicallyOrderedAdd` `Ordinal.isAcc_iff`

Ordinal.IsClosedBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Ordinal` `Set` `Set.instMembership`	—	`Ordinal.isClosedBelow_iff`
`iInter` 📖	mathematical	`Ordinal.IsClosedBelow`	`Ordinal.IsClosedBelow` `Set.iInter` `Ordinal`	—	`sInter`
`sInter` 📖	mathematical	`Ordinal.IsClosedBelow`	`Ordinal.IsClosedBelow` `Set.sInter` `Ordinal`	—	`Ordinal.isClosedBelow_iff` `forall_lt` `Ordinal.IsAcc.mono` `Set.sInter_subset_of_mem`

---

← Back to Index