cast_lt

Mathlib.Data.Nat.Cast.Order.Basic

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

English

For all m,n ∈ ℕ, (m : α) < n iff m < n.

Русский

Для всех m,n ∈ ℕ, (m : α) < n эквивалентно m < n.

LaTeX

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

Lean4

@[simp, norm_cast, mono]
theorem cast_lt : (m : α) < n ↔ m < n :=
  strictMono_cast.lt_iff_lt

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

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

Разделы

Аффилиация

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