finsetCard_eq — Mathlib

English

If a function induces a bijection between two finite sets, then the sets have the same cardinality.

Русский

Если функция задаёт биекцию между двумя конечными множествами, то их кардинальности равны.

LaTeX

$$$BijOn(e, s, t) \Rightarrow |s| = |t|$$$

Lean4

theorem _root_.Set.BijOn.finsetCard_eq (e : α → β) (he : Set.BijOn e s t) : #s = #t :=
  card_nbij e he.mapsTo he.injOn he.surjOn

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