mem_antidiagonal — Mathlib

English

A pair x belongs to antidiagonal n if and only if its components sum to n.

Русский

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

LaTeX

$$$x \in \mathrm{antidiagonal}(n) \\Leftrightarrow x.1 + x.2 = n$$$

Lean4

/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
@[simp]
theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n :=
  by
  rw [antidiagonal, mem_map]; constructor
  · rintro ⟨i, hi, rfl⟩
    rw [mem_range, Nat.lt_succ_iff] at hi
    exact Nat.add_sub_cancel' hi
  · rintro rfl
    refine ⟨x.fst, ?_, ?_⟩
    · rw [mem_range]
      cutsat
    · exact Prod.ext rfl (by simp only [Nat.add_sub_cancel_left])

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