toENat_le_nat

Mathlib.SetTheory.Cardinal.ENat

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

English

Alternate presentation of ENat ≤ Nat: toENat x ≤ n iff x ≤ n, as above.

Русский

Альтернативное представление: toENat x ≤ n эквивалентно x ≤ n.

LaTeX

$$$\\forall x \\in \\mathrm{Cardinal},\\forall n \\in \\mathbb{N},\\ toENat(x) \\le n \\iff x \\le n$$$

Lean4

@[simp]
theorem toENat_le_nat {a : Cardinal} {n : ℕ} : toENat a ≤ n ↔ a ≤ n :=
  toENatAux_le_nat

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

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

Разделы

Аффилиация

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