card_image_diag — Mathlib

English

For any finite set s, the cardinality of the image of its diagonal under the Sym2.mk map equals the cardinality of s.

Русский

Для любого конечного множества s число элементов образа диагонали под отображением Sym2.mk равно числу элементов s.

LaTeX

$$$\#(s.\mathrm{diag}.\mathrm{image} \; \mathrm{Sym2.mk}) = \#s$$$

Lean4

/-- The `diag` of `s : Finset α` is sent on a finset of `Sym2 α` of card `#s`. -/
theorem card_image_diag (s : Finset α) : #(s.diag.image Sym2.mk) = #s :=
  by
  rw [card_image_of_injOn, diag_card]
  rintro ⟨x₀, x₁⟩ hx _ _ h
  cases Sym2.eq.1 h
  · rfl
  · simp only [mem_coe, mem_diag] at hx
    rw [hx.2]

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