Indexed

📁 Source: Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean

Statistics

Metric	Count
Definitions	0
Theorems Ici_ciSup, Iic_ciInf, ciInf_eq_of_forall_ge_of_forall_gt_exists_lt, ciInf_le_ciSup, ciInf_le_of_le, ciInf_mono, ciSup_eq_of_forall_le_of_forall_lt_exists_gt, ciSup_le_iff, ciSup_mono, isGLB_ciInf, isLUB_ciSup, le_ciInf_iff, le_ciSup_of_le, ciInf_set_le, ciSup_set_le_iff, isGLB_ciInf_set, isLUB_ciSup_set, le_ciInf_set_iff, le_ciSup_set, l_ciSup_of_directed, l_ciSup_set_of_directedOn, l_csSup_of_directedOn, l_csSup_of_directedOn', u_ciInf_of_directed, u_ciInf_set_of_directedOn, u_csInf_of_directedOn, u_csInf_of_directedOn', ciSup_mem_iInter_Icc_of_antitone, map_ciInf_of_directed, map_ciInf_set_of_directedOn, map_ciSup_of_directed, map_ciSup_set_of_directedOn, map_csInf_of_directedOn, map_csInf_of_directedOn', map_csSup_of_directedOn, map_csSup_of_directedOn', cbiInf_eq_of_forall, cbiSup_eq_of_forall, ciInf_Ici, ciInf_const, ciInf_eq_ite, ciInf_neg, ciInf_pos, ciInf_subsingleton, ciInf_unique, ciSup_Iic, ciSup_const, ciSup_eq_ite, ciSup_mem_iInter_Icc_of_antitone_Icc, ciSup_neg, ciSup_pos, ciSup_subsingleton, ciSup_unique	53
Total	53

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ici_ciSup 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder BddAbove Set.range	Set.Ici iSup ConditionallyCompletePartialOrderSup.toSupSet Set.iInter	—	Set.ext ciSup_le_iff
Iic_ciInf 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder BddBelow Set.range	Set.Iic iInf ConditionallyCompletePartialOrderInf.toInfSet Set.iInter	—	Set.ext Set.mem_Iic Set.mem_iInter le_ciInf_iff
ciInf_eq_of_forall_ge_of_forall_gt_exists_lt 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Preorder.toLT	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt directedOn_range Set.range_nonempty Set.forall_mem_range Set.exists_range_iff
ciInf_le_ciSup 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup BddBelow Set.range BddAbove	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf iSup ConditionallyCompletePartialOrderSup.toSupSet	—	LE.le.trans ciInf_le le_ciSup
ciInf_le_of_le 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder BddBelow Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	ge_trans ciInf_le
ciInf_mono 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder BddBelow Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	isEmpty_or_nonempty iInf_of_isEmpty le_refl le_ciInf ciInf_le_of_le
ciSup_eq_of_forall_le_of_forall_lt_exists_gt 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Preorder.toLT	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt directedOn_range Set.range_nonempty Set.forall_mem_range Set.exists_range_iff
ciSup_le_iff 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder BddAbove Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	isLUB_le_iff isLUB_ciSup Set.forall_mem_range
ciSup_mono 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder BddAbove Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	isEmpty_or_nonempty iSup_of_empty' le_refl ciSup_le le_ciSup_of_le
isGLB_ciInf 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder BddBelow Set.range	IsGLB iInf ConditionallyCompletePartialOrderInf.toInfSet	—	DirectedOn.isGLB_csInf directedOn_range Set.range_nonempty
isLUB_ciSup 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder BddAbove Set.range	IsLUB iSup ConditionallyCompletePartialOrderSup.toSupSet	—	DirectedOn.isLUB_csSup directedOn_range Set.range_nonempty
le_ciInf_iff 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder BddBelow Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	le_isGLB_iff isGLB_ciInf Set.forall_mem_range
le_ciSup_of_le 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder BddAbove Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	le_trans le_ciSup

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ciInf_set_le 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Set.image BddBelow Set Set.instMembership	iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet	—	LE.le.trans_eq' csInf_le Set.mem_image_of_mem sInf_image'
ciSup_set_le_iff 📖	mathematical	Set.Nonempty DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Set.image BddAbove	iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	isLUB_le_iff isLUB_ciSup_set Set.forall_mem_image
isGLB_ciInf_set 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Set.image BddBelow Set.Nonempty	IsGLB iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet Set Set.instMembership	—	sInf_image' isGLB_csInf Set.Nonempty.image
isLUB_ciSup_set 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Set.image BddAbove Set.Nonempty	IsLUB iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	sSup_image' isLUB_csSup Set.Nonempty.image
le_ciInf_set_iff 📖	mathematical	Set.Nonempty DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Set.image BddBelow	iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet Set Set.instMembership	—	le_isGLB_iff isGLB_ciInf_set Set.forall_mem_image
le_ciSup_set 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Set.image BddAbove Set Set.instMembership	iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet	—	LE.le.trans_eq le_csSup Set.mem_image_of_mem sSup_image'

GaloisConnection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
l_ciSup_of_directed 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Directed Preorder.toLE BddAbove Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	iSup.eq_1 l_csSup_of_directedOn Directed.directedOn_range Set.range_nonempty iSup_range'
l_ciSup_set_of_directedOn 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder DirectedOn Preorder.toLE Set.image BddAbove Set.Nonempty	iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	l_ciSup_of_directed Set.Nonempty.to_subtype Set.range_comp Subtype.range_coe_subtype Set.image_eq_range
l_csSup_of_directedOn 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder DirectedOn Preorder.toLE Set.Nonempty BddAbove	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet iSup Set.Elem Set Set.instMembership	—	Set.range_comp Subtype.range_coe_subtype l_csSup_of_directedOn'
l_csSup_of_directedOn' 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder DirectedOn Preorder.toLE Set.Nonempty BddAbove	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	IsLUB.unique isLUB_l_image DirectedOn.isLUB_csSup DirectedOn.mono_comp monotone_l Set.Nonempty.image Monotone.map_bddAbove
u_ciInf_of_directed 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Directed Preorder.toLE BddBelow Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	l_ciSup_of_directed dual
u_ciInf_set_of_directedOn 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder DirectedOn Preorder.toLE Set.image BddBelow Set.Nonempty	iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet Set Set.instMembership	—	l_ciSup_set_of_directedOn dual
u_csInf_of_directedOn 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder DirectedOn Preorder.toLE Set.Nonempty BddBelow	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet iInf Set.Elem Set Set.instMembership	—	l_csSup_of_directedOn dual
u_csInf_of_directedOn' 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder DirectedOn Preorder.toLE Set.Nonempty BddBelow	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet Set.image	—	l_csSup_of_directedOn' dual

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ciSup_mem_iInter_Icc_of_antitone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Antitone Pi.hasLe Preorder.toLE	Set Set.instMembership Set.iInter Set.Icc iSup ConditionallyCompletePartialOrderSup.toSupSet	—	Set.mem_iInter forall_le_of_antitone directed_le Directed.le_ciSup Set.forall_mem_range Directed.ciSup_le

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_ciInf_of_directed 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder BddBelow Set.range	DFunLike.coe OrderIso instFunLikeOrderIso iInf ConditionallyCompletePartialOrderInf.toInfSet	—	map_ciSup_of_directed
map_ciInf_set_of_directedOn 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Set.image BddBelow Set.Nonempty	DFunLike.coe OrderIso instFunLikeOrderIso iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet Set Set.instMembership	—	map_ciSup_set_of_directedOn
map_ciSup_of_directed 📖	mathematical	Directed Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder BddAbove Set.range	DFunLike.coe OrderIso instFunLikeOrderIso iSup ConditionallyCompletePartialOrderSup.toSupSet	—	GaloisConnection.l_ciSup_of_directed to_galoisConnection
map_ciSup_set_of_directedOn 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Set.image BddAbove Set.Nonempty	DFunLike.coe OrderIso instFunLikeOrderIso iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	GaloisConnection.l_ciSup_set_of_directedOn to_galoisConnection
map_csInf_of_directedOn 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Set.Nonempty BddBelow	DFunLike.coe OrderIso instFunLikeOrderIso InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet iInf Set.Elem Set Set.instMembership	—	map_csSup_of_directedOn
map_csInf_of_directedOn' 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder Set.Nonempty BddBelow	DFunLike.coe OrderIso instFunLikeOrderIso InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet Set.image	—	map_csSup_of_directedOn'
map_csSup_of_directedOn 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Set.Nonempty BddAbove	DFunLike.coe OrderIso instFunLikeOrderIso SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet iSup Set.Elem Set Set.instMembership	—	GaloisConnection.l_csSup_of_directedOn to_galoisConnection
map_csSup_of_directedOn' 📖	mathematical	DirectedOn Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder Set.Nonempty BddAbove	DFunLike.coe OrderIso instFunLikeOrderIso SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	GaloisConnection.l_csSup_of_directedOn' to_galoisConnection

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cbiInf_eq_of_forall 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	iInf_congr_Prop ciInf_unique Set.Subset.antisymm Set.mem_range
cbiSup_eq_of_forall 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	iSup_congr_Prop ciSup_unique Set.Subset.antisymm
ciInf_Ici 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderInf.toPartialOrder	iInf Set.Elem Set.Ici ConditionallyCompletePartialOrderInf.toInfSet Set Set.instMembership	—	le_refl Set.mem_range Set.mem_Ici LE.le.antisymm Directed.ciInf_le Directed.le_ciInf_iff Set.nonempty_Ici_subtype
ciInf_const 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	iInf.eq_1 Set.range_const csInf_singleton
ciInf_eq_ite 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet InfSet.sInf Set Set.instEmptyCollection	—	iInf_congr_Prop ciInf_unique ciInf_neg
ciInf_neg 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet InfSet.sInf Set Set.instEmptyCollection	—	iInf.eq_1 Set.range_eq_empty_iff isEmpty_Prop
ciInf_pos 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	iInf_congr_Prop ciInf_unique
ciInf_subsingleton 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet	—	ciInf_unique
ciInf_unique 📖	mathematical	—	iInf ConditionallyCompletePartialOrderInf.toInfSet Unique.instInhabited	—	Unique.eq_default ciInf_const
ciSup_Iic 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder	iSup Set.Elem Set.Iic ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	le_refl LE.le.antisymm' Directed.le_ciSup Directed.ciSup_le_iff Set.nonempty_Iic_subtype
ciSup_const 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	iSup.eq_1 Set.range_const csSup_singleton
ciSup_eq_ite 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet SupSet.sSup Set Set.instEmptyCollection	—	iSup_congr_Prop ciSup_unique ciSup_neg
ciSup_mem_iInter_Icc_of_antitone_Icc 📖	mathematical	Antitone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra Set.Icc ConditionallyCompletePartialOrderSup.toPartialOrder Preorder.toLE	Set.instMembership Set.iInter iSup ConditionallyCompletePartialOrderSup.toSupSet	—	Monotone.ciSup_mem_iInter_Icc_of_antitone Set.Icc_subset_Icc_iff
ciSup_neg 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet SupSet.sSup Set Set.instEmptyCollection	—	iSup.eq_1 Set.range_eq_empty_iff isEmpty_Prop
ciSup_pos 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	iSup_congr_Prop ciSup_unique
ciSup_subsingleton 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	ciSup_unique
ciSup_unique 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet Unique.instInhabited	—	Unique.eq_default ciSup_const

---

← Back to Index