English
For any z in the symmetric square, the cardinality of its associated finite set equals 1 if z is diagonal and 2 otherwise.
Русский
Для любого z в симметрической квадрате кардинал связного с z конечного множества равен 1, если z диагонален, иначе 2.
LaTeX
$$$\\forall \\alpha\\, (z : \\mathrm{Sym}^2(\\alpha)),\\; \\#\\bigl(z : \\mathrm{Sym}^2(\\alpha)\\bigr) .\\mathrm{toFinset} = \\text{ite } z.IsDiag 1 2$$$
Lean4
/-- Mapping an unordered pair to a finite set produces a finset of size `1` if the pair is on the
diagonal, else of size `2` if the pair is off the diagonal. -/
theorem card_toFinset (z : Sym2 α) : #(z : Sym2 α).toFinset = if z.IsDiag then 1 else 2 :=
by
by_cases h : z.IsDiag
· simp [card_toFinset_of_isDiag z h, h]
· simp [card_toFinset_of_not_isDiag z h, h]
