ofENatHom

Mathlib.SetTheory.Cardinal.ENat

URI: https://scilib.ai/kg/mathlib#Cardinal.ofENatHom

← MathLib Explorer

English

If α ≃ β, then toENat #α = toENat #β.

Русский

Если α эквивалентно β, то toENat #α = toENat #β.

LaTeX

$$$toENat(#\\alpha) = toENat(#\\beta)$$$

Lean4

/-- The coercion `Cardinal.ofENat` as a bundled homomorphism. -/
def ofENatHom : ℕ∞ →+*o Cardinal where
  toFun := (↑)
  map_one' := ofENat_one
  map_mul' := ofENat_mul
  map_zero' := ofENat_zero
  map_add' := ofENat_add
  monotone' := ofENat_mono

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

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

Разделы

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

Аффилиация

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