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