Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-28 17:22 89d8cc37

View on Github →

refactor(data/nat/basic): review API of nat.find_greatest (#4274) Other changes:

  • add nat.find_eq_iff;
  • use weaker assumptions in measurable_to_encodable and measurable_to_nat;
  • add measurable_find.

Estimated changes

added theorem nat.find_eq_iff
deleted theorem nat.find_greatest_eq_zero
modified theorem nat.find_greatest_le
modified theorem nat.find_greatest_spec
added theorem measurable_find
modified theorem measurable_find_greatest