mem_antidiagonalTuple — Mathlib

English

An element x belongs to antidiagonalTuple k n iff the sum of its coordinates is n.

Русский

Элемент x принадлежит antidiagonalTuple k n тогда и только тогда, когда сумма координат x равна n.

LaTeX

$$$ x \\in antidiagonalTuple k n \\iff \\sum i, x(i) = n $$$

Lean4

theorem mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} : x ∈ antidiagonalTuple k n ↔ ∑ i, x i = n := by
  induction x using Fin.consInduction generalizing n with
  | elim0 =>
    cases n
    · decide
    · simp
  | cons x₀ x ih =>
    simp_rw [Fin.sum_cons, antidiagonalTuple, List.mem_flatMap, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_inj,
      exists_eq_right_right, ih, @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ←
      Prod.mk_inj (a₁ := Prod.fst _), exists_eq_right]

Похожие утверждения