Commit 2022-04-10 12:36 83225b3d

View on Github →

feat(order/monovary): Add missing monovary lemmas (#13243) Add lemmas for postcomposing monovarying functions with monotone/antitone functions. Protect lemmas that needed it. Fix typos.

Estimated changes

Modified src/order/monovary.lean

added theorem antivary.comp_antitone_left

added theorem antivary.comp_monotone_left

modified theorem antivary.dual

modified theorem antivary.dual_left

modified theorem antivary.dual_right

added theorem antivary_on.comp_antitone_on_left

added theorem antivary_on.comp_antitone_on_right

added theorem antivary_on.comp_monotone_on_left

added theorem antivary_on.comp_monotone_on_right

added theorem antivary_on.comp_right

modified theorem antivary_on.dual

modified theorem antivary_on.dual_left

modified theorem antivary_on.dual_right

added theorem antivary_on.empty

added theorem monovary.comp_antitone_left

added theorem monovary.comp_monotone_left

modified theorem monovary.dual

modified theorem monovary.dual_left

modified theorem monovary.dual_right

added theorem monovary_on.comp_antitone_on_left

added theorem monovary_on.comp_antitone_on_right

added theorem monovary_on.comp_monotone_on_left

added theorem monovary_on.comp_monotone_on_right

added theorem monovary_on.comp_right

modified theorem monovary_on.dual

modified theorem monovary_on.dual_left

modified theorem monovary_on.dual_right

added theorem monovary_on.empty

modified theorem monovary_on_self

deleted theorem subsingleton.antivary

deleted theorem subsingleton.antivary_on

deleted theorem subsingleton.monovary

deleted theorem subsingleton.monovary_on