IsNormal

📁 Source: Mathlib/Order/IsNormal.lean

Statistics

Metric	Count
Definitions	0
Theorems isNormal, apply_of_isSuccLimit, comp, exists_map_le_lt_map_succ, exists_map_le_lt_map_succ_of_exists_ge, ext, ext_iff, id, isLUB_image_Iio_of_isSuccLimit, le_iff_forall_le, le_iff_le_sSup, le_iff_le_sSup', lt_iff_exists_lt, map_iSup, map_isLUB, map_isSuccLimit, map_sSup, mem_lowerBounds_upperBounds_of_isSuccLimit, monotone, of_succ_lt, preimage_Iic, strictMono, to_Iio, isNormal_iff, isNormal_iff', isNormal, isNormal	27
Total	27

InitialSeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNormal 📖	mathematical	—	Order.IsNormal DFunLike.coe InitialSeg Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLike	—	strictMono image_Iio Order.IsSuccLimit.isLUB_Iio map_isSuccLimit

Order

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNormal_iff 📖	mathematical	—	IsNormal StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	—
isNormal_iff' 📖	mathematical	—	IsNormal StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership lowerBounds Preorder.toLE upperBounds Set.image Set.Iio	—	—

Order.IsNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_of_isSuccLimit 📖	mathematical	Order.IsNormal ConditionallyCompleteLinearOrder.toLinearOrder ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Order.IsSuccLimit PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	iSup Set.Elem Set.Iio PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	Order.IsSuccLimit.iSup_Iio map_iSup Order.IsSuccLimit.bot_lt LT.lt.le
comp 📖	mathematical	Order.IsNormal	Order.IsNormal	—	StrictMono.comp strictMono le_iff_forall_le map_isSuccLimit lt_iff_exists_lt LE.le.trans LT.lt.le Set.image_congr
exists_map_le_lt_map_succ 📖	mathematical	Order.IsNormal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Order.succ	—	exists_map_le_lt_map_succ_of_exists_ge StrictMono.le_apply strictMono
exists_map_le_lt_map_succ_of_exists_ge 📖	mathematical	Order.IsNormal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Order.succ	—	StrictMono.le_iff_le strictMono LE.le.trans le_iff_le_sSup le_refl not_le Order.lt_succ_iff
ext 📖	mathematical	Order.IsNormal	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ	—	ext_iff
ext_iff 📖	mathematical	Order.IsNormal	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ	—	IsMin.eq_bot IsLUB.unique isLUB_image_Iio_of_isSuccLimit Set.ext
id 📖	mathematical	—	Order.IsNormal	—	OrderIso.isNormal
isLUB_image_Iio_of_isSuccLimit 📖	mathematical	Order.IsNormal Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.image Set.Iio	—	LT.lt.le strictMono mem_lowerBounds_upperBounds_of_isSuccLimit
le_iff_forall_le 📖	mathematical	Order.IsNormal Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isLUB_le_iff isLUB_image_Iio_of_isSuccLimit
le_iff_le_sSup 📖	mathematical	Order.IsNormal ConditionallyCompleteLinearOrder.toLinearOrder Set.Nonempty Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice BddAbove Preorder.toLE	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.preimage Set.Iic	—	Set.ext_iff preimage_Iic
le_iff_le_sSup' 📖	mathematical	Order.IsNormal ConditionallyCompleteLinearOrder.toLinearOrder Set.Nonempty Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.preimage Set.Iic	—	le_iff_le_sSup LE.le.trans StrictMono.le_apply strictMono
lt_iff_exists_lt 📖	mathematical	Order.IsNormal Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	lt_isLUB_iff isLUB_image_Iio_of_isSuccLimit
map_iSup 📖	mathematical	Order.IsNormal ConditionallyCompleteLinearOrder.toLinearOrder BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	Set.ext map_sSup Set.range_nonempty
map_isLUB 📖	mathematical	Order.IsNormal IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.image	—	StrictMono.le_iff_le strictMono IsLUB.isSuccLimit_of_notMem le_iff_forall_le IsLUB.exists_between LE.le.trans LT.lt.le
map_isSuccLimit 📖	mathematical	Order.IsNormal Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_isMin_iff Order.IsSuccLimit.not_isMin strictMono lt_iff_exists_lt CovBy.lt CovBy.ge_of_gt LT.lt.not_ge StrictMono.le_iff_le
map_sSup 📖	mathematical	Order.IsNormal ConditionallyCompleteLinearOrder.toLinearOrder Set.Nonempty BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.image	—	IsLUB.csSup_eq map_isLUB isLUB_csSup Set.Nonempty.image
mem_lowerBounds_upperBounds_of_isSuccLimit 📖	mathematical	Order.IsNormal Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership lowerBounds Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder upperBounds Set.image Set.Iio	—	—
monotone 📖	mathematical	Order.IsNormal	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	StrictMono.monotone strictMono
of_succ_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ IsLUB Preorder.toLE Set.image Set.Iio	Order.IsNormal	—	IsMin.not_lt Order.lt_succ_iff_eq_or_lt_of_not_isMax LT.lt.trans Order.IsSuccLimit.succ_lt LT.lt.trans_le Order.lt_succ_of_not_isMax LT.lt.not_isMax Set.mem_image_of_mem
preimage_Iic 📖	mathematical	Order.IsNormal ConditionallyCompleteLinearOrder.toLinearOrder Set.Nonempty Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice BddAbove Preorder.toLE	Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	le_antisymm le_csSup LE.le.lt_or_eq lt_csSup_iff LE.le.trans LT.lt.le strictMono Set.mem_preimage map_sSup csSup_le_csSup bddAbove_Iic Set.image_preimage_subset csSup_Iic le_refl
strictMono 📖	mathematical	Order.IsNormal	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
to_Iio 📖	mathematical	Order.IsNormal	Order.IsNormal Set.Elem Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.instLinearOrder Set Set.instMembership strictMono	—	strictMono Order.isNormal_iff mem_lowerBounds_upperBounds_of_isSuccLimit Order.IsSuccLimit.subtypeVal isLowerSet_Iio LT.lt.trans

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNormal 📖	mathematical	—	Order.IsNormal DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderIso	—	InitialSeg.isNormal

PrincipalSeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNormal 📖	mathematical	—	Order.IsNormal DFunLike.coe RelEmbedding Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder RelEmbedding.instFunLike toRelEmbedding	—	InitialSeg.isNormal mem_range_of_rel instIsTransLt

---

← Back to Index