card_subtype_not_diag — Mathlib

English

The number of non-diagonal elements in Sym2 α equals (card α).choose 2.

Русский

Число не диагональных элементов в Sym2 α равно (card α).choose 2.

LaTeX

$$$|\{ a:\!\ Sym2\alpha \;\mid\; ¬a.\mathrm{IsDiag}\}| = { |\alpha| \choose 2 }$$$

Lean4

theorem card_subtype_not_diag [Fintype α] : card { a : Sym2 α // ¬a.IsDiag } = (card α).choose 2 :=
  by
  convert card_image_offDiag (univ : Finset α)
  rw [← filter_image_mk_not_isDiag, Fintype.card_of_subtype]
  rintro x
  rw [mem_filter, univ_product_univ, mem_image]
  obtain ⟨a, ha⟩ := Quot.exists_rep x
  exact and_iff_right ⟨a, mem_univ _, ha⟩

Похожие утверждения