card_of_bijective

Mathlib.Data.Fintype.Card

URI: https://scilib.ai/kg/mathlib#Fintype.card_of_bijective

English

If f: α → β is a bijection between finite types α and β, then the cardinalities are equal: |α| = |β|.

Русский

Если отображение f: α → β биективно, то кардинальности множеств α и β равны: |α| = |β|.

LaTeX

$$$|\\alpha| = |\\beta|$$$

Lean4

theorem card_of_bijective {f : α → β} (hf : Bijective f) : card α = card β :=
  card_congr (Equiv.ofBijective f hf)

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

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

Разделы

Аффилиация

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