English
Let z be an unordered pair in the symmetric square that lies on the diagonal. Then the finite set associated to z has exactly one element.
Русский
Пусть z является неупорядоченной парой в симметрической квадрате и лежит на диагонали. Тогда конечное множество, связанное с z, содержит ровно один элемент.
LaTeX
$$$\\forall \\alpha\\, (z : \\mathrm{Sym}^2(\\alpha)),\\; z\\text{ IsDiag }\\Rightarrow \\#\\bigl(z : \\mathrm{Sym}^2(\\alpha)\\bigr) .\\mathrm{toFinset} = 1$$$
Lean4
/-- Mapping an unordered pair on the diagonal to a finite set produces a finset of size `1`. -/
theorem card_toFinset_of_isDiag (z : Sym2 α) (h : z.IsDiag) : #(z : Sym2 α).toFinset = 1 :=
by
induction z
rw [Sym2.mk_isDiag_iff] at h
simp [Sym2.toFinset_mk_eq, h]
