toNat_add

Mathlib.SetTheory.Cardinal.ToNat

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

← MathLib Explorer

English

If c < aleph0 and d < aleph0, then toNat(c + d) = toNat(c) + toNat(d).

Русский

Если c < ℵ0 и d < ℵ0, то toNat(c + d) = toNat(c) + toNat(d).

LaTeX

$$$\forall {c,d} (hc : c < \aleph_0) (hd : d < \aleph_0),\ toNat(c + d) = toNat(c) + toNat(d).$$$

Lean4

@[simp]
theorem toNat_add (hc : c < ℵ₀) (hd : d < ℵ₀) : toNat (c + d) = toNat c + toNat d :=
  by
  lift c to ℕ using hc
  lift d to ℕ using hd
  norm_cast

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

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

Разделы

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

Аффилиация

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