English
There is a natural equivalence between the antidiagonal n and Fin(n+1) given by the first projection.
Русский
Существует естественное эквивалентность между антидиагональю n и Fin(n+1), заданная проекцией по первой координате.
LaTeX
$$antidiagonal(n) ≃ Fin(n+1)$$
Lean4
@[simp]
theorem antidiagonal_filter_snd_le_of_le {n k : ℕ} (h : k ≤ n) :
{a ∈ antidiagonal n | a.snd ≤ k} =
(antidiagonal k).map (Embedding.prodMap ⟨_, add_left_injective (n - k)⟩ (Embedding.refl ℕ)) :=
by
ext ⟨i, j⟩
suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa
refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
· rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2, add_tsub_cancel_right]
· rintro ⟨l, hl, rfl⟩
refine ⟨?_, hl ▸ Nat.le_add_left j l⟩
rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
exact Nat.sub_add_cancel h
