Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-04 03:33 4cca114a

View on Github →

feat(data/fin): fin.find (#1167)

  • feat(data/fin): fin.find
  • add nat_find_mem_find

Estimated changes

added def fin.find
added theorem fin.find_eq_none_iff
added theorem fin.find_min'
added theorem fin.find_min
added theorem fin.find_spec
added theorem fin.is_some_find_iff
added theorem fin.nat_find_mem_find