Fin.eq_of_veq
theorem Fin.eq_of_veq : ∀ {n : ℕ} {i j : Fin n}, ↑i = ↑j → i = j
This theorem, `Fin.eq_of_veq`, states that for any natural number `n`, and any two elements `i` and `j` of the finite set `Fin n`, if the natural number representations of `i` and `j` (obtained using the up-arrow `↑` operator) are equal, then `i` and `j` themselves are also equal. Essentially, this asserts that the equality of the natural number representations of two elements in a finite set implies the equality of the elements themselves.
More concisely: For any finite set `Fin n` and elements `i`, `j` in `Fin n`, `i = j` if and only if `↑i = ↑j`.
|
Fin.veq_of_eq
theorem Fin.veq_of_eq : ∀ {n : ℕ} {i j : Fin n}, i = j → ↑i = ↑j
This theorem states that for any natural number 'n' and any two finite numbers 'i' and 'j' within the range 0 to 'n-1' (represented as 'Fin n'), if 'i' is equal to 'j', then the natural number representation of 'i' (denoted as ↑i) is equal to the natural number representation of 'j' (denoted as ↑j). Essentially, it guarantees that equality between two `Fin n` elements also implies equality between their corresponding natural numbers.
More concisely: For any natural number n and all i, j in Fin n (0 <= i, j < n), i = j implies ↑i = ↑j.
|