card_image_equiv — Mathlib

English

If e : α ≃ β is a bijection, then for every subset S of α, the cardinality of e(S) equals the cardinality of S.

Русский

Пусть e : α ≃ β — биекция. Тогда для каждого подмножества S ⊆ α кардинальность образа e(S) равна кардинальности S.

LaTeX

$$$$ \forall S \subseteq \alpha, \; |e[S]| = |S| $$$$

Lean4

theorem card_image_equiv (e : α ≃ β) : Nat.card (e '' s) = Nat.card s :=
  Nat.card_congr (e.image s).symm

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