antidiagonalTuple_one — Mathlib

English

The 0-tuple with sum n+1 is empty (again).

Русский

Повторение: 0-tuple сумма n+1 пуст.

LaTeX

$$$ antidiagonalTuple 0 (n+1) = [] $$$

Lean4

@[simp]
theorem antidiagonalTuple_one (n : ℕ) : antidiagonalTuple 1 n = [![n]] :=
  by
  simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton, Nat.sub_self,
    List.flatMap_append, List.flatMap_singleton, List.flatMap_map]
  conv_rhs => rw [← List.nil_append [![n]]]
  congr 1
  simp_rw [List.flatMap_eq_nil_iff, List.mem_range, List.map_eq_nil_iff]
  intro x hx
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx
  rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]

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