English
The non-diagonal elements obtained by mapping the product s × s under mk correspond to the off-diagonal part of s.
Русский
Не диагональные элементы, полученные через отображение mk из s × s, соответствуют вне диагонали.
LaTeX
$$$\\forall (s: \\mathrm{Finset}(\\alpha))\\; {\\{a \\in (s \\times^s s).image \\mathrm{mk} \\mid \\lnot a.IsDiag\\} = s.offDiag.image \\mathrm{mk}}$$$
Lean4
theorem filter_image_mk_not_isDiag [DecidableEq α] (s : Finset α) :
{a ∈ (s ×ˢ s).image Sym2.mk | ¬a.IsDiag} = s.offDiag.image Sym2.mk :=
by
ext z
induction z
simp only [mem_image, mem_offDiag, mem_filter, Prod.exists, mem_product]
constructor
· rintro ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩
rw [← h, Sym2.mk_isDiag_iff] at hab
exact ⟨a, b, ⟨ha, hb, hab⟩, h⟩
· rintro ⟨a, b, ⟨ha, hb, hab⟩, h⟩
rw [Ne, ← Sym2.mk_isDiag_iff, h] at hab
exact ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩
