card_eq_of_equiv_fin

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_eq_of_equiv_fin

← MathLib Explorer

English

If f : α ≃ Fin n, then Nat.card α = n.

Русский

Если существует эквивалентность α с Fin n, то Nat.card α = n.

LaTeX

$$$ \forall f : \alpha \simeq \mathrm{Fin}\,n, \mathrm{Nat.card}\alpha = n $$$

Lean4

theorem card_eq_of_equiv_fin {α : Type*} {n : ℕ} (f : α ≃ Fin n) : Nat.card α = n := by
  simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f

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

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

Разделы

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

Аффилиация

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