CompleteLatticeIntervals

📁 Source: Mathlib/Order/CompleteLatticeIntervals.lean

Statistics

Metric	Count
Definitions completeLattice, instCompleteLattice, instCompleteLinearOrderElemIccOfFactLe, ordConnectedSubsetConditionallyCompleteLinearOrder, subsetConditionallyCompleteLinearOrder, subsetInfSet, subsetSupSet	7
Theorems coe_iInf, coe_iSup, coe_sInf, coe_sSup, coe_biInf, coe_biSup, coe_iInf, coe_iSup, coe_sInf, coe_sSup, sInf_within_of_ordConnected, sSup_within_of_ordConnected, subset_sInf_def, subset_sInf_emptyset, subset_sInf_of_not_bddBelow, subset_sInf_of_within, subset_sSup_def, subset_sSup_emptyset, subset_sSup_of_not_bddAbove, subset_sSup_of_within	20
Total	27

Set.Icc

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	4 math math: coe_sSup, coe_iInf, coe_sInf, coe_iSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_iInf 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	Set Set.instMembership Set.Icc iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf CompleteLattice.toConditionallyCompleteLattice completeLattice	—	coe_sInf Set.range_nonempty Set.range_comp
coe_iSup 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	Set Set.instMembership Set.Icc iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet CompleteLattice.toConditionallyCompleteLattice completeLattice	—	coe_sSup Set.range_nonempty Set.range_comp
coe_sInf 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty Set.Elem Set.Icc	Set Set.instMembership InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf CompleteLattice.toConditionallyCompleteLattice completeLattice Set.image	—	Set.Nonempty.ne_empty
coe_sSup 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty Set.Elem Set.Icc	Set Set.instMembership SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet CompleteLattice.toConditionallyCompleteLattice completeLattice Set.image	—	Set.Nonempty.ne_empty

Set.Iic

Definitions

Name	Category	Theorems
instCompleteLattice 📖	CompOp	8 math math: coe_sInf, coe_iInf, coe_biInf, coe_sSup, instIsCompactlyGenerated, coe_iSup, iSupIndep.of_coe_Iic_comp, coe_biSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_biInf 📖	mathematical	—	Set Set.instMembership Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf instCompleteLattice SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	isEmpty_or_nonempty coe_iInf inf_of_le_left inf_idem
coe_biSup 📖	mathematical	—	Set Set.instMembership Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet instCompleteLattice	—	coe_iSup
coe_iInf 📖	mathematical	—	Set Set.instMembership Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf instCompleteLattice SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	iInf.eq_1 coe_sInf Set.ext
coe_iSup 📖	mathematical	—	Set Set.instMembership Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet instCompleteLattice	—	iSup.eq_1 coe_sSup Set.ext
coe_sInf 📖	mathematical	—	Set Set.instMembership Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice InfSet.sInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf instCompleteLattice SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.image	—	—
coe_sSup 📖	mathematical	—	Set Set.instMembership Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice SupSet.sSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet instCompleteLattice Set.image	—	—

(root)

Definitions

Name	Category	Theorems
instCompleteLinearOrderElemIccOfFactLe 📖	CompOp	—
ordConnectedSubsetConditionallyCompleteLinearOrder 📖	CompOp	—
subsetConditionallyCompleteLinearOrder 📖	CompOp	—
subsetInfSet 📖	CompOp	4 math math: subset_sInf_of_not_bddBelow, subset_sInf_emptyset, subset_sInf_of_within, subset_sInf_def
subsetSupSet 📖	CompOp	4 math math: subset_sSup_emptyset, subset_sSup_of_within, subset_sSup_of_not_bddAbove, subset_sSup_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sInf_within_of_ordConnected 📖	mathematical	Set.Nonempty Set.Elem BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	Set.OrdConnected.out Monotone.le_csInf_image Subtype.mono_coe Monotone.csInf_image_le
sSup_within_of_ordConnected 📖	mathematical	Set.Nonempty Set.Elem BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	Set.OrdConnected.out Monotone.le_csSup_image Subtype.mono_coe Monotone.csSup_image_le
subset_sInf_def 📖	mathematical	—	InfSet.sInf Set.Elem subsetInfSet Set.Nonempty BddBelow Preorder.toLE Set Set.instMembership Set.image	—	—
subset_sInf_emptyset 📖	mathematical	—	InfSet.sInf Set.Elem subsetInfSet Set Set.instEmptyCollection	—	Set.image_empty
subset_sInf_of_not_bddBelow 📖	mathematical	BddBelow Set.Elem Preorder.toLE Set Set.instMembership	InfSet.sInf subsetInfSet	—	—
subset_sInf_of_within 📖	mathematical	Set.Nonempty Set.Elem BddBelow Preorder.toLE Set Set.instMembership InfSet.sInf Set.image	subsetInfSet	—	—
subset_sSup_def 📖	mathematical	—	SupSet.sSup Set.Elem subsetSupSet Set.Nonempty BddAbove Preorder.toLE Set Set.instMembership Set.image	—	—
subset_sSup_emptyset 📖	mathematical	—	SupSet.sSup Set.Elem subsetSupSet Set Set.instEmptyCollection	—	Set.image_empty
subset_sSup_of_not_bddAbove 📖	mathematical	BddAbove Set.Elem Preorder.toLE Set Set.instMembership	SupSet.sSup subsetSupSet	—	—
subset_sSup_of_within 📖	mathematical	Set.Nonempty Set.Elem BddAbove Preorder.toLE Set Set.instMembership SupSet.sSup Set.image	subsetSupSet	—	—

---

← Back to Index