strictMono

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.strictMono

English

The embedding f is strictly increasing: if a < a' then f(a) < f(a').

Русский

Встроенное отображение строго возрастает: если a < a', то f(a) < f(a').

LaTeX

$$$a < a' \Rightarrow f(a) < f(a')$$$

Lean4

theorem strictMono [PartialOrder α] (f : α ≤i β) : StrictMono f :=
  f.toOrderEmbedding.strictMono

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

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

Разделы

Аффилиация

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