natCast_le_natCast

Mathlib.Data.Nat.Cast.Order.Basic

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

English

Let a,b be natural numbers with a ≤ b. Then their images in α satisfy (a : α) ≤ (b : α).

Русский

Пусть a,b — натуральные числа и a ≤ b. Тогда их образы в α удовлетворяют (a : α) ≤ (b : α).

LaTeX

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

Lean4

@[gcongr]
theorem _root_.GCongr.natCast_le_natCast {a b : ℕ} (h : a ≤ b) : (a : α) ≤ b :=
  mono_cast h

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

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

Разделы

Аффилиация

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