OrdContinuous

📁 Source: Mathlib/Order/OrdContinuous.lean

Statistics

Metric	Count
Definitions LeftOrdContinuous, toOrderEmbedding, RightOrdContinuous, toOrderEmbedding	4
Theorems leftOrdContinuous, rightOrdContinuous, coe_toOrderEmbedding, comp, id, iterate, le_iff, lt_iff, map_ciSup, map_csSup, map_iSup, map_isGreatest, map_sSup, map_sSup', map_sup, mono, rightOrdContinuous_dual, leftOrdContinuous, rightOrdContinuous, coe_toOrderEmbedding, comp, id, iterate, le_iff, lt_iff, map_ciInf, map_csInf, map_iInf, map_inf, map_isLeast, map_sInf, map_sInf', mono, orderDual	34
Total	38

GaloisConnection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftOrdContinuous 📖	mathematical	GaloisConnection	LeftOrdContinuous	—	isLUB_l_image
rightOrdContinuous 📖	mathematical	GaloisConnection	RightOrdContinuous	—	isGLB_u_image

LeftOrdContinuous

Definitions

Name	Category	Theorems
toOrderEmbedding 📖	CompOp	1 math math: coe_toOrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toOrderEmbedding 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder SemilatticeSup.toPartialOrder	DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding toOrderEmbedding	—	—
comp 📖	—	LeftOrdContinuous	—	—	Set.image_image
id 📖	mathematical	—	LeftOrdContinuous	—	Set.image_id
iterate 📖	mathematical	LeftOrdContinuous	Nat.iterate	—	id comp
le_iff 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder SemilatticeSup.toPartialOrder	Preorder.toLE	—	map_sup
lt_iff 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder SemilatticeSup.toPartialOrder	Preorder.toLT	—	le_iff
map_ciSup 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddAbove Preorder.toLE Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	map_csSup Set.range_nonempty
map_csSup 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty BddAbove Preorder.toLE	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	IsLUB.csSup_eq isLUB_csSup Set.Nonempty.image
map_iSup 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	map_sSup'
map_isGreatest 📖	mathematical	LeftOrdContinuous IsGreatest Preorder.toLE	Set.image	—	Set.mem_image_of_mem IsGreatest.isLUB
map_sSup 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet iSup Set Set.instMembership	—	map_sSup' sSup_image
map_sSup' 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	IsLUB.sSup_eq isLUB_sSup
map_sup 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder SemilatticeSup.toPartialOrder	SemilatticeSup.toMax	—	IsLUB.unique isLUB_pair Set.image_pair
mono 📖	mathematical	LeftOrdContinuous	Monotone	—	upperBounds_insert upperBounds_singleton map_isGreatest Set.mem_image_of_mem
rightOrdContinuous_dual 📖	mathematical	LeftOrdContinuous	RightOrdContinuous OrderDual OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual OrderDual.ofDual	—	—

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftOrdContinuous 📖	mathematical	—	LeftOrdContinuous DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso	—	GaloisConnection.leftOrdContinuous to_galoisConnection
rightOrdContinuous 📖	mathematical	—	RightOrdContinuous DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso	—	GaloisConnection.rightOrdContinuous to_galoisConnection

RightOrdContinuous

Definitions

Name	Category	Theorems
toOrderEmbedding 📖	CompOp	1 math math: coe_toOrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toOrderEmbedding 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder SemilatticeInf.toPartialOrder	DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding toOrderEmbedding	—	—
comp 📖	—	RightOrdContinuous	—	—	LeftOrdContinuous.comp orderDual
id 📖	mathematical	—	RightOrdContinuous	—	Set.image_id
iterate 📖	mathematical	RightOrdContinuous	Nat.iterate	—	LeftOrdContinuous.iterate orderDual
le_iff 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder SemilatticeInf.toPartialOrder	Preorder.toLE	—	LeftOrdContinuous.le_iff orderDual
lt_iff 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder SemilatticeInf.toPartialOrder	Preorder.toLT	—	LeftOrdContinuous.lt_iff orderDual
map_ciInf 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddBelow Preorder.toLE Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	LeftOrdContinuous.map_ciSup orderDual
map_csInf 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty BddBelow Preorder.toLE	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	LeftOrdContinuous.map_csSup orderDual
map_iInf 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	LeftOrdContinuous.map_iSup orderDual
map_inf 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder SemilatticeInf.toPartialOrder	SemilatticeInf.toMin	—	LeftOrdContinuous.map_sup orderDual
map_isLeast 📖	mathematical	RightOrdContinuous IsLeast Preorder.toLE	Set.image	—	LeftOrdContinuous.map_isGreatest orderDual
map_sInf 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf iInf Set Set.instMembership	—	LeftOrdContinuous.map_sSup orderDual
map_sInf' 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	LeftOrdContinuous.map_sSup' orderDual
mono 📖	mathematical	RightOrdContinuous	Monotone	—	Monotone.dual LeftOrdContinuous.mono orderDual
orderDual 📖	mathematical	RightOrdContinuous	LeftOrdContinuous OrderDual OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual OrderDual.ofDual	—	—

(root)

Definitions

Name	Category	Theorems
LeftOrdContinuous 📖	MathDef	4 math math: RightOrdContinuous.orderDual, GaloisConnection.leftOrdContinuous, LeftOrdContinuous.id, OrderIso.leftOrdContinuous
RightOrdContinuous 📖	MathDef	4 math math: LeftOrdContinuous.rightOrdContinuous_dual, RightOrdContinuous.id, OrderIso.rightOrdContinuous, GaloisConnection.rightOrdContinuous

---

← Back to Index