toENat_le_one

Mathlib.SetTheory.Cardinal.ENat

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

English

The comparison to 1 is preserved: toENat a ≤ 1 iff a ≤ 1.

Русский

Сохранение сравнения с единицей: toENat a ≤ 1 эквивалентно a ≤ 1.

LaTeX

$$$\\forall a \\in \\mathrm{Cardinal},\\ toENat(a) \\le 1 \\iff a \\le 1$$$

Lean4

@[simp]
theorem toENat_le_one {a : Cardinal} : toENat a ≤ 1 ↔ a ≤ 1 :=
  toENat_le_nat

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

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

Разделы

Аффилиация

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