PiLex

📁 Source: Mathlib/Order/CompleteLattice/PiLex.lean

Statistics

Metric	Count
Definitions completeLattice, instCompleteLinearOrderColexForall, instInfSetColexForall, instSupSetColexForall, completeLattice, instCompleteLinearOrderLexForall, instInfSetLexForall, instSupSetLexForall	8
Theorems le_sInf_apply, le_sSup_apply, sInf_apply, sInf_apply_le, sSup_apply, sSup_apply_le, le_sInf_apply, le_sSup_apply, sInf_apply, sInf_apply_le, sSup_apply, sSup_apply_le	12
Total	20

Pi.Colex

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	—
instCompleteLinearOrderColexForall 📖	CompOp	—
instInfSetColexForall 📖	CompOp	2 math math: le_sInf_apply, sInf_apply
instSupSetColexForall 📖	CompOp	2 math math: sSup_apply, sSup_apply_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_sInf_apply 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	InfSet.sInf Colex instInfSetColexForall	—	Pi.Lex.le_sInf_apply IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT
le_sSup_apply 📖	mathematical	Colex Set Set.instMembership SupSet.sSup instSupSetColexForall	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	Pi.Lex.le_sSup_apply IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT
sInf_apply 📖	mathematical	—	InfSet.sInf Colex instInfSetColexForall iInf Set.Elem setOf Set Set.instMembership ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	Pi.Lex.sInf_apply IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT
sInf_apply_le 📖	mathematical	Colex Set Set.instMembership InfSet.sInf instInfSetColexForall	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	Pi.Lex.sInf_apply_le IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT
sSup_apply 📖	mathematical	—	SupSet.sSup Colex instSupSetColexForall iSup Set.Elem setOf Set Set.instMembership ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	Pi.Lex.sSup_apply IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT
sSup_apply_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	SupSet.sSup Colex instSupSetColexForall	—	Pi.Lex.sSup_apply_le IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT

Pi.Lex

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	—
instCompleteLinearOrderLexForall 📖	CompOp	—
instInfSetLexForall 📖	CompOp	2 math math: sInf_apply, le_sInf_apply
instSupSetLexForall 📖	CompOp	2 math math: sSup_apply_le, sSup_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_sInf_apply 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	InfSet.sInf Lex instInfSetLexForall	—	sInf_apply le_sInf
le_sSup_apply 📖	mathematical	Lex Set Set.instMembership SupSet.sSup instSupSetLexForall	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	sInf_apply_le
sInf_apply 📖	mathematical	—	InfSet.sInf Lex instInfSetLexForall iInf Set.Elem setOf Set Set.instMembership ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	—
sInf_apply_le 📖	mathematical	Lex Set Set.instMembership InfSet.sInf instInfSetLexForall	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	sInf_apply sInf_le
sSup_apply 📖	mathematical	—	SupSet.sSup Lex instSupSetLexForall iSup Set.Elem setOf Set Set.instMembership ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	—	sInf_apply
sSup_apply_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot	SupSet.sSup Lex instSupSetLexForall	—	le_sInf_apply

---

← Back to Index