cast_le_ofNat

Mathlib.Data.Nat.Cast.Order.Basic

URI: https://scilib.ai/kg/mathlib#Nat.cast_le_ofNat

English

Same as Cast_lt_ofNat above: the strict order is preserved when casting Nat to α via ofNat.

Русский

То же самое, что и выше: строгий порядок сохраняется при привидении Nat к α через ofNat.

LaTeX

$$$\forall m,n \in \mathbb{N},\ (m : \alpha) < (ofNat(n) : \alpha) \iff m < OfNat.ofNat n.$$$

Lean4

@[simp]
theorem cast_le_ofNat : (m : α) ≤ (ofNat(n) : α) ↔ m ≤ OfNat.ofNat n :=
  cast_le

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

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

Разделы

Аффилиация

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