one_toNat

Mathlib.SetTheory.Cardinal.ToNat

URI: https://scilib.ai/kg/mathlib#Cardinal.one_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) < \operatorname{toNat}(d) \iff c < d.$$$

Lean4

theorem one_toNat : toNat 1 = 1 :=
  map_one _

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

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

Разделы

Аффилиация

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