Commit 2022-12-30 10:55 f1cd87ba

View on Github →

feat: port Order.SemiconjSup (#1265)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SemiconjSup.lean

added theorem Function.Semiconj.symm_adjoint

added theorem Function.csupₛ_div_semiconj

added theorem Function.semiconj_of_isLUB

added theorem Function.supₛ_div_semiconj

added theorem IsOrderRightAdjoint.comp_orderIso

added theorem IsOrderRightAdjoint.orderIso_comp

added theorem IsOrderRightAdjoint.right_mono

added def IsOrderRightAdjoint

added theorem isOrderRightAdjoint_csupₛ

added theorem isOrderRightAdjoint_supₛ