English
There is an equivalence between antidiagonal n and Fin(n+1); the maps are explicit: toFun ⟨⟨i,_⟩, h⟩ ↦ ⟨i, fst_lt h⟩ and invFun ⟨i,h⟩ ↦ ⟨⟨i, n−i⟩, proof⟩.
Русский
Существует явная эквивалентность между антидиагональю n и Fin(n+1): отображение вперед задано как ⟨⟨i,_⟩, h⟩ ↦ ⟨i, fst_lt h⟩, обратное как ⟨i,h⟩ ↦ ⟨⟨i, n−i⟩, доказательство⟩.
LaTeX
$$antidiagonalEquivFin(n) : antidiagonal n ≃ Fin (n+1)$$
Lean4
/-- The set `antidiagonal n` is equivalent to `Fin (n+1)`, via the first projection. -/
@[simps]
def antidiagonalEquivFin (n : ℕ) : antidiagonal n ≃ Fin (n + 1)
where
toFun := fun ⟨⟨i, _⟩, h⟩ ↦ ⟨i, antidiagonal.fst_lt h⟩
invFun := fun ⟨i, h⟩ ↦
⟨⟨i, n - i⟩, by
rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]
exact Nat.le_of_lt_succ h⟩
