strictMono_cast

Mathlib.Data.Nat.Cast.Order.Basic

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

English

The map n ↦ (n : α) is strictly increasing: if m < n then (m : α) < (n : α).

Русский

Отображение n ↦ (n : α) strictly возрастает: если m < n, то (m : α) < (n : α).

LaTeX

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

Lean4

theorem strictMono_cast : StrictMono (Nat.cast : ℕ → α) :=
  mono_cast.strictMono_of_injective cast_injective

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

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

Разделы

Аффилиация

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