card_eq_coe_natCard

Mathlib.Data.Finite.Card

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

← MathLib Explorer

English

For finite α, ENat.card α equals Nat.card α, after coercion to ENat.

Русский

Для конечного α: ENat.card α равен Nat.card α после приведения к ENat.

LaTeX

$$ENat.card(\alpha) = (Nat.card(\alpha)).cast$$

Lean4

theorem card_eq_coe_natCard (α : Type*) [Finite α] : card α = Nat.card α :=
  by
  unfold ENat.card
  apply symm
  rw [Cardinal.natCast_eq_toENat_iff]
  exact Nat.cast_card

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

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

Разделы

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

Аффилиация

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