English
The subset of the antidiagonal with a fixed first coordinate m is either the singleton { (m, n−m) } if m ≤ n, or empty otherwise.
Русский
Подмножество антидиагонали с фиксированной первой координатой m равно либо одинокому элементу { (m, n−m) } при m ≤ n, либо пустому множеству иначе.
LaTeX
$$$\\{x \\in \\operatorname{antidiagonal}(n) \\mid x_1 = m\\} = \\begin{cases} \\{(m, n-m)\\} & \\text{если } m \\le n \\\\ \\emptyset & \\text{иначе} \\end{cases}$$$
Lean4
theorem filter_fst_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
{x ∈ antidiagonal n | x.fst = m} = if m ≤ n then {(m, n - m)} else ∅ :=
by
ext ⟨a, b⟩
suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
by
rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton, Prod.mk_inj, ite_prop_iff_or]
simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]
rintro rfl
constructor
· rintro rfl
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
· rintro ⟨h, rfl⟩
exact add_tsub_cancel_of_le h
