natCast_lt_natCast

Mathlib.Data.Nat.Cast.Order.Basic

URI: https://scilib.ai/kg/mathlib#GCongr.natCast_lt_natCast

English

If a < b in ℕ, then (a : α) < (b : α).

Русский

Если a < b в ℕ, то (a : α) < (b : α).

LaTeX

$$$\forall a,b \in \mathbb{N},\ a < b \Rightarrow (a : \alpha) < (b : \alpha).$$$

Lean4

@[gcongr]
theorem _root_.GCongr.natCast_lt_natCast {a b : ℕ} (h : a < b) : (a : α) < b :=
  strictMono_cast h

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

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

Разделы

Аффилиация

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