CompleteLattice

📁 Source: Mathlib/Algebra/Order/Group/CompleteLattice.lean

Statistics

Metric	Count
Definitions	0
Theorems add_ciInf, add_ciSup, ciInf_add, ciInf_div, ciInf_mul, ciInf_sub, ciSup_add, ciSup_div, ciSup_mul, ciSup_sub, mul_ciInf, mul_ciSup	12
Total	12

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_ciInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	OrderIso.map_ciInf
add_ciSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet	—	OrderIso.map_ciSup
ciInf_add 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	OrderIso.map_ciInf
ciInf_div 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	DivInvMonoid.toDiv Group.toDivInvMonoid iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	div_eq_mul_inv ciInf_mul
ciInf_mul 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	OrderIso.map_ciInf
ciInf_sub 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	SubNegMonoid.toSub AddGroup.toSubNegMonoid iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	sub_eq_add_neg ciInf_add
ciSup_add 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet	—	OrderIso.map_ciSup
ciSup_div 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	DivInvMonoid.toDiv Group.toDivInvMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet	—	div_eq_mul_inv ciSup_mul
ciSup_mul 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet	—	OrderIso.map_ciSup
ciSup_sub 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	SubNegMonoid.toSub AddGroup.toSubNegMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet	—	sub_eq_add_neg ciSup_add
mul_ciInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	OrderIso.map_ciInf
mul_ciSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet	—	OrderIso.map_ciSup

---

← Back to Index