mathlib3
7f4286c9 - chore(order/basic): add `le_update_iff` and `update_le_iff` (#5080)

Commit
5 years ago
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.
Author
Parents
Loading