card_eq_of_bijective

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_eq_of_bijective

English

If f is bijective, Nat.card α = Nat.card β.

Русский

Если f биективно отображает α на β, то кардиналы равны.

LaTeX

$$$ \forall {\alpha\, \beta} (f : \alpha \to \beta), \mathrm{Bijective}\,f \rightarrow \mathrm{Nat.card}\alpha = \mathrm{Nat.card}\beta $$$

Lean4

theorem card_eq_of_bijective (f : α → β) (hf : Function.Bijective f) : Nat.card α = Nat.card β :=
  card_congr (Equiv.ofBijective f hf)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru