Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-22 22:06 7f4286c9

View on Github →

chore(order/basic): add le_update_iff and update_le_iff (#5080) Other changes:

  • add update_eq_iff, eq_update_iff and a more general lemma rel_update_iff;
  • remove @[simps] attributes on pi.*_lattice instances.

Estimated changes

added theorem function.eq_update_iff
added theorem function.update_eq_iff
added theorem le_update_iff
added theorem update_le_iff