natCast_strictMono

Mathlib.Algebra.Order.Group.Unbundled.Int

URI: https://scilib.ai/kg/mathlib#Int.natCast_strictMono

English

The natural embedding ℕ → ℤ is strictly increasing.

Русский

Естественное вложение ℕ в ℤ строго возрастает.

LaTeX

$$$ \text{StrictMono}((\cdot : \mathbb{N} \to \mathbb{Z}))$.$$

Lean4

theorem natCast_strictMono : StrictMono (· : ℕ → ℤ) := fun _ _ ↦ Int.ofNat_lt.2

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

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

Разделы

Аффилиация

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