card_inv — Mathlib

English

Let α have decidable equality and an involutive inversion. For any finite s, the cardinality of s⁻¹ equals the cardinality of s.

Русский

Пусть α имеет разрешимое равенство и инволюцию обращения. Для любого конечного множества s, кардинальность s⁻¹ равна кардинальности s.

LaTeX

$$$#s^{-1} = #s$$$

Lean4

@[to_additive (attr := simp)]
theorem card_inv (s : Finset α) : #s⁻¹ = #s :=
  card_image_of_injective _ inv_injective

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