English
The diagonal elements obtained by mapping the product s × s under the diagonal-mapping function coincide with the image of the diagonal of s under mk.
Русский
Диагональные элементы, полученные через отображение произведения s × s под диагональным отображением, совпадают с изображением диагонали s под mk.
LaTeX
$$$\\forall (s: \\mathrm{Finset}(\\alpha))\\; {\\{a \\in (s \\times^s s).image \\mathrm{mk} \\mid a.IsDiag\\} = s.diag.image \\mathrm{mk}}$$$
Lean4
theorem filter_image_mk_isDiag [DecidableEq α] (s : Finset α) :
{a ∈ (s ×ˢ s).image Sym2.mk | a.IsDiag} = s.diag.image Sym2.mk :=
by
ext ⟨x, y⟩
simp only [mem_image, mem_diag, 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, hab⟩, h⟩
· rintro ⟨a, b, ⟨ha, rfl⟩, h⟩
rw [← h]
exact ⟨⟨a, a, ⟨ha, ha⟩, rfl⟩, rfl⟩
