zero_toNat

Mathlib.SetTheory.Cardinal.ToNat

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

English

For finite cardinals c,d, toNat c ≤ toNat d iff c ≤ d.

Русский

Для конечных кардиналов c,d: toNat c ≤ toNat d ⇔ c ≤ d.

LaTeX

$$$\forall c,d \in Iio(\aleph_0): \operatorname{toNat}(c) \le \operatorname{toNat}(d) \iff c \le d.$$$

Lean4

@[simp]
theorem zero_toNat : toNat 0 = 0 :=
  map_zero _

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

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

Разделы

Аффилиация

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