card_congr

Mathlib.SetTheory.Cardinal.Finite

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

English

If f is an equivalence between α and β, Nat.card α = Nat.card β.

Русский

Если существует эквивалентность между α и β, то кардиналы равны.

LaTeX

$$$ \forall f : \alpha \to \beta, \mathrm{Equiv}\,\alpha\beta \Rightarrow \mathrm{Nat.card}\alpha = \mathrm{Nat.card}\beta $$$

Lean4

theorem card_congr (f : α ≃ β) : Nat.card α = Nat.card β :=
  Cardinal.toNat_congr f

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

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

Разделы

Аффилиация

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