toNat_eq_ofNat

Mathlib.SetTheory.Cardinal.ToNat

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

← MathLib Explorer

English

If c < d and d is finite, then toNat c < toNat d.

Русский

Если c < d и d конечен, то toNat c < toNat d.

LaTeX

$$$\forall {c d : \mathrm{Cardinal}},\ c < d \land d < \aleph_0 \Rightarrow toNat c < toNat d.$$$

Lean4

/-- A version of `toNat_eq_iff` for literals -/
theorem toNat_eq_ofNat {n : ℕ} [Nat.AtLeastTwo n] : toNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n :=
  toNat_eq_iff <| OfNat.ofNat_ne_zero n

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

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

Разделы

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

Аффилиация

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