toNat_eq_iff

Mathlib.SetTheory.Cardinal.ToNat

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

English

For any cardinals c ≤ d with d finite, toNat(c) ≤ toNat(d).

Русский

Для любых кардиналов c ≤ d, где d конечен, toNat(c) ≤ toNat(d).

LaTeX

$$$\forall {c,d:\mathbb{Cardinal}},\ c \le d \to d < \aleph_0 \Rightarrow toNat c \le toNat d.$$$

Lean4

theorem toNat_eq_iff {n : ℕ} (hn : n ≠ 0) : toNat c = n ↔ c = n := by
  rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_nat]

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

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

Разделы

Аффилиация

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