Documentation Verification Report

IsNormal

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

Statistics

Metric	Count
Definitions `IsNormal`, `IsNormal`, `IsNormal`	3
Theorems `continuous`, `isNormal_iff_strictMono_and_continuous`	2
Total	5

CategoryTheory.Subgroupoid

Definitions

Name	Category	Theorems
`IsNormal` 📖	CompData	4 math math: `generatedNormal_isNormal`, `ker_isNormal`, `discrete_isNormal`, `top_isNormal`

Order

Definitions

Name	Category	Theorems
`IsNormal` 📖	CompData	30 math math: `Ordinal.isNormal_mul_right`, `OrderIso.isNormal`, `Cardinal.isNormal_preAleph`, `InitialSeg.isNormal`, `Ordinal.isNormal_veblen`, `IsNormal.of_succ_lt`, `Ordinal.isNormal_iff_lt_succ_and_bsup_eq`, `Ordinal.isNormal_preOmega`, `Ordinal.isNormal_opow`, `isNormal_iff_strictMono_and_continuous`, `Ordinal.isNormal_deriv`, `Cardinal.isNormal_aleph`, `Ordinal.isNormal_enumOrd`, `Ordinal.isNormal_iff_lt_succ_and_blsub_eq`, `Ordinal.isNormal_veblen_zero`, `Ordinal.isNormal_derivFamily`, `Ordinal.isNormal_gamma`, `PrincipalSeg.isNormal`, `isNormal_iff'`, `Ordinal.enumOrd_isNormal_iff_isClosed`, `Ordinal.isNormal_veblenWith'`, `isNormal_iff`, `Cardinal.isNormal_beth`, `Ordinal.isNormal_add_right`, `Cardinal.isNormal_preBeth`, `Cardinal.isNormal_ord`, `IsNormal.id`, `Ordinal.IsNormal.trans`, `Ordinal.isNormal_iff_strictMono_and_continuous`, `Ordinal.isNormal_omega`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNormal_iff_strictMono_and_continuous` 📖	mathematical	—	`IsNormal` `StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Continuous`	—	`IsNormal.strictMono` `IsNormal.continuous` `isLUB_of_mem_closure` `LT.lt.le` `image_closure_subset_closure_image` `Set.mem_image_of_mem` `IsLUB.mem_closure` `IsSuccLimit.isLUB_Iio` `Set.Iio_nonempty`

Order.IsNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	`Order.IsNormal`	`Continuous`	—	`OrderTopology.continuous_iff` `isClosed_compl_iff` `Set.preimage_compl` `Set.compl_Ioi` `IsLowerSet.eq_univ_or_Iio` `IsLowerSet.preimage` `isLowerSet_Iic` `StrictMono.monotone` `strictMono` `isClosed_univ` `Set.eq_empty_or_nonempty` `isClosed_empty` `preimage_Iic` `bddAbove_Iio` `isClosed_Iic` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `IsLowerSet.isOpen` `isLowerSet_Iio`

Ordinal

Definitions

Name	Category	Theorems
`IsNormal` 📖	MathDef	2 math math: `isNormal_iff_strictMono_limit`, `IsNormal.refl`

---

← Back to Index