mathlib
89d8cc37 - refactor(data/nat/basic): review API of `nat.find_greatest` (#4274)

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