SemiconjSup

📁 Source: Mathlib/Order/SemiconjSup.lean

Statistics

Metric	Count
Definitions IsOrderRightAdjoint	1
Theorems symm_adjoint, csSup_div_semiconj, sSup_div_semiconj, semiconj_of_isLUB, comp_orderIso, orderIso_comp, right_mono, unique, isOrderRightAdjoint_csSup, isOrderRightAdjoint_sSup	10
Total	11

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
csSup_div_semiconj 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range DFunLike.coe OrderIso instFunLikeOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid RelIso.instGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Semiconj iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder instFunLikeOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid RelIso.instGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	—	semiconj_of_isLUB isLUB_csSup Set.range_nonempty One.instNonempty
sSup_div_semiconj 📖	mathematical	—	Semiconj iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder instFunLikeOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid RelIso.instGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	—	semiconj_of_isLUB isLUB_iSup
semiconj_of_isLUB 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder Set.range DFunLike.coe OrderIso instFunLikeOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid RelIso.instGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Semiconj DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RelIso.instGroup MonoidHom.instFunLike	—	IsLUB.unique OrderIso.leftOrdContinuous map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_inv_rev RelIso.apply_inv_self Surjective.range_comp Equiv.surjective Set.range_comp

Function.Semiconj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symm_adjoint 📖	mathematical	Function.Semiconj DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso OrderEmbedding instFunLikeOrderEmbedding IsOrderRightAdjoint	Function.Semiconj DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding OrderIso PartialOrder.toPreorder instFunLikeOrderIso	—	IsLUB.unique Function.Surjective.image_preimage OrderIso.surjective Set.preimage_setOf_eq eq OrderEmbedding.le_iff_le OrderIso.leftOrdContinuous

IsOrderRightAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_orderIso 📖	mathematical	IsOrderRightAdjoint	IsOrderRightAdjoint DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm	—	OrderIso.isLUB_preimage OrderIso.apply_symm_apply
orderIso_comp 📖	mathematical	IsOrderRightAdjoint	IsOrderRightAdjoint DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm	—	OrderIso.le_symm_apply
right_mono 📖	mathematical	IsOrderRightAdjoint	Monotone	—	IsLUB.mono le_trans
unique 📖	—	IsOrderRightAdjoint PartialOrder.toPreorder	—	—	IsLUB.unique

(root)

Definitions

Name	Category	Theorems
IsOrderRightAdjoint 📖	MathDef	4 math math: IsOrderRightAdjoint.comp_orderIso, isOrderRightAdjoint_csSup, isOrderRightAdjoint_sSup, IsOrderRightAdjoint.orderIso_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrderRightAdjoint_csSup 📖	mathematical	Preorder.toLE BddAbove PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder setOf	IsOrderRightAdjoint PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet setOf Preorder.toLE	—	isLUB_csSup
isOrderRightAdjoint_sSup 📖	mathematical	—	IsOrderRightAdjoint PartialOrder.toPreorder CompleteSemilatticeSup.toPartialOrder SupSet.sSup CompleteSemilatticeSup.toSupSet setOf Preorder.toLE	—	isLUB_sSup

---

← Back to Index