Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 13:47 65e2411a

View on Github →

feat(order/bounds): is_lub/is_glb in Pi types and product types (#8583)

  • Add monotone_fst and monotone_snd.
  • Add some trivial lemmas about upper_bounds and lower_bounds.
  • Turn is_lub_pi and is_glb_pi into iff lemmas.
  • Add is_lub_prod and is_glb_prod.
  • Fix some header levels in module docs of order/bounds.

Estimated changes

added theorem monotone_fst
added theorem monotone_snd
added theorem is_glb_iff_le_iff
modified theorem is_glb_pi
added theorem is_glb_prod
added theorem is_glb_upper_bounds
added theorem is_lub_iff_le_iff
added theorem is_lub_lower_bounds
modified theorem is_lub_pi
added theorem is_lub_prod