ofEquiv_card

Mathlib.Data.Fintype.Card

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

English

Given a finite α and an equivalence f : α ≃ β, the cardinality of β equals the cardinality of α.

Русский

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

LaTeX

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

Lean4

theorem ofEquiv_card [Fintype α] (f : α ≃ β) : @card β (ofEquiv α f) = card α :=
  Multiset.card_map _ _

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

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

Разделы

Аффилиация

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