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	—	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	—	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 📖	—	Function.Semiconj DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso OrderEmbedding instFunLikeOrderEmbedding IsOrderRightAdjoint	—	—	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	DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm	—	OrderIso.isLUB_preimage OrderIso.apply_symm_apply
orderIso_comp 📖	mathematical	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	2 math math: isOrderRightAdjoint_csSup, isOrderRightAdjoint_sSup

Theorems

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

---

← Back to Index