card_congr

Mathlib.SetTheory.Cardinal.Finite

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

English

If f is a bijection between α and β, then ENat.card α = ENat.card β.

Русский

Если существует биекция между α и β, то ENat.card α = ENat.card β.

LaTeX

$$$\operatorname{ENat}.card(\alpha) = \operatorname{ENat}.card(\beta)$$$

Lean4

theorem card_congr {α β : Type*} (f : α ≃ β) : card α = card β :=
  Cardinal.toENat_congr f

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

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

Разделы

Аффилиация

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