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	8 math math: generatedNormal_isNormal, isNormal_map, ker_isNormal, discrete_isNormal, top_isNormal, isNormal_comap, disconnect_normal, sInf_isNormal

Order

Definitions

Name	Category	Theorems
IsNormal 📖	CompData	35 math math: Ordinal.IsNormal.veblenWith, Ordinal.isNormal_mul_right, OrderIso.isNormal, Cardinal.isNormal_preAleph, InitialSeg.isNormal, Ordinal.isNormal_veblen, Ordinal.isNormal_veblenWith, IsNormal.of_succ_lt, IsNormal.to_Iio, 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, IsNormal.comp, Cardinal.isNormal_beth, Ordinal.isNormal_add_right, Cardinal.isNormal_preBeth, Cardinal.isNormal_ord, IsNormal.id, Ordinal.IsNormal.trans, Ordinal.isNormal_veblenWith_zero, Ordinal.IsNormal.veblenWith_zero, 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