card_eq_of_equiv_fintype

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Finset.card_eq_of_equiv_fintype

← MathLib Explorer

English

If i : s ≃ Fin n, then |s| = n.

Русский

Если i : s ≃ Fin n, то |s| = n.

LaTeX

$${i : s ≃ Fin n} → |s| = n$$

Lean4

theorem card_eq_of_equiv_fintype {s : Finset α} [Fintype β] (i : s ≃ β) : #s = Fintype.card β :=
  card_eq_of_equiv_fin <| i.trans <| Fintype.equivFin β

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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