Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-05 12:32 365e30de

View on Github →

chore(data/set/,order/): add missing lemmas about monotone_on etc (#14943)

  • Add monotone_on/antitone/antitone_on versions of existing monotone lemmas for id/const, inf/sup/min/max, inter/union, and intervals.
  • Drop set.monotone_prod, leave monotone.set_prod only.
  • Golf some proofs that were broken by removal of set.monotone_prod.

Estimated changes

added theorem antitone_on.inter
added theorem antitone_on.union
added theorem monotone_on.inter
added theorem monotone_on.union
deleted theorem set.monotone_prod
added theorem antitone.set_prod
added theorem antitone_on.set_prod
added theorem monotone.set_prod
added theorem monotone_on.set_prod
added theorem antitone_on_const
added theorem monotone_on_const
added theorem monotone_on_id
added theorem strict_mono_on_id
added theorem nhds_eq_uniformity'