Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-02 06:13 1494cc14

View on Github →

feat(order/semiconj_Sup): use Sup to semiconjugate functions (#2895) Formalize two lemmas from a paper by É. Ghys.

Estimated changes

Modified docs/references.bib

Modified src/order/bounds.lean

added theorem is_glb.mono

added theorem is_greatest.mono

added theorem is_least.mono

added theorem is_lub.mono

Modified src/order/complete_lattice.lean

Created src/order/semiconj_Sup.lean

added theorem function.Sup_div_semiconj

added theorem function.cSup_div_semiconj

added theorem function.semiconj.symm_adjoint

added theorem function.semiconj_of_is_lub

added theorem is_order_right_adjoint.right_mono

added theorem is_order_right_adjoint.unique

added def is_order_right_adjoint

added theorem is_order_right_adjoint_Sup

added theorem is_order_right_adjoint_cSup