card_congr

Mathlib.Data.Fintype.Card

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

English

For an equivalence f : α ≃ β, the cardinalities of α and β are equal.

Русский

При эквивалентности f : α ≃ β кардинал α равен кардиналу β.

LaTeX

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

Lean4

theorem card_congr {α β} [Fintype α] [Fintype β] (f : α ≃ β) : card α = card β := by rw [← ofEquiv_card f]; congr!

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

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

Разделы

Аффилиация

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