Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-27 05:22 a7e34357

View on Github →

chore(data/option): swap sides in ne_none_iff_exists (#4285)

  • swap lhs and rhs of the equality in option.ne_none_iff_exists; the new order matches, e.g., the definition of set.range and can_lift.prf;
  • the same in with_one.ne_one_iff_exists and with_zero.ne_zero_iff_exists;
  • remove option.ne_none_iff_exists';
  • restore the original option.ne_none_iff_exists as option.ne_none_iff_exists'

Estimated changes

modified theorem with_one.ne_one_iff_exists
modified theorem option.ne_none_iff_exists'
modified theorem option.ne_none_iff_exists