toENat_congr

Mathlib.SetTheory.Cardinal.ENat

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem toENat_congr {α : Type u} {β : Type v} (e : α ≃ β) : toENat #α = toENat #β := by
  rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]

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

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

Разделы

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

Аффилиация

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