Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-15 07:43 0bb283b8

View on Github →

feat(algebra/bounds): add csupr_mul etc (#8584)

  • add csupr_mul, mul_csupr, csupr_div, csupr_add, mul_csupr, add_csupr, csupr_sub;
  • add is_lub_csupr, is_lub_csupr_set, is_glb_cinfi, is_glb_cinfi_set;
  • add is_lub.csupr_eq, is_lub.csupr_set_eq, is_glb.cinfi_eq, is_glb.cinfi_set_eq;
  • add is_greatest.Sup_mem, is_least.Inf_mem;
  • add lemmas about galois_connection and Sup/Inf in conditionally complete lattices;
  • add lemmas about order_iso and Sup/Inf in conditionally complete lattices.

Estimated changes

added theorem csupr_div
added theorem csupr_mul
added theorem mul_csupr
added theorem is_glb.cinfi_eq
added theorem is_glb.cinfi_set_eq
added theorem is_glb_cinfi
added theorem is_glb_cinfi_set
added theorem is_greatest.Sup_mem
added theorem is_least.Inf_mem
added theorem is_lub.csupr_eq
added theorem is_lub.csupr_set_eq
added theorem is_lub_csupr
added theorem is_lub_csupr_set
added theorem order_iso.map_cInf
added theorem order_iso.map_cSup
added theorem order_iso.map_cinfi
added theorem order_iso.map_csupr