Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-11 22:44 7fdd4f37

View on Github →

refactor(data/nat/nth): redefine, review API (#18760) Redefine nat.nth in terms of already available definitions, review API, generalize some lemmas. Also fix some typos in data/set/intervals/monotone.

Estimated changes

added theorem nat.count_nth
deleted theorem nat.count_nth_gc
added theorem nat.count_nth_succ
added theorem nat.gc_count_nth
added theorem nat.image_nth_Iio_card
added theorem nat.is_least_nth
added theorem nat.le_nth
added theorem nat.le_nth_count'
added theorem nat.le_nth_count
modified theorem nat.le_nth_of_count_le
modified theorem nat.nth_count_eq_Inf
deleted theorem nat.nth_count_le
added theorem nat.nth_eq_Inf
added theorem nat.nth_eq_nthd_sort
modified theorem nat.nth_eq_order_iso_of_nat
added theorem nat.nth_eq_zero
added theorem nat.nth_eq_zero_mono
added theorem nat.nth_inj_on
added theorem nat.nth_injective
added theorem nat.nth_le_nth'
added theorem nat.nth_le_nth
added theorem nat.nth_lt_nth'
added theorem nat.nth_lt_nth
modified theorem nat.nth_lt_of_lt_count
added theorem nat.nth_mem
modified theorem nat.nth_mem_of_infinite
added theorem nat.nth_mem_of_lt_card
deleted theorem nat.nth_mono_of_finite
modified theorem nat.nth_monotone
added theorem nat.nth_of_card_le
deleted theorem nat.nth_set_card
deleted theorem nat.nth_set_card_aux
modified theorem nat.nth_strict_mono
added theorem nat.nth_strict_mono_on
modified theorem nat.nth_zero
deleted theorem nat.nth_zero_of_nth_zero
modified theorem nat.nth_zero_of_zero
added theorem nat.range_nth_subset
added theorem nat.subset_range_nth