strictMono_of_injective

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#Monotone.strictMono_of_injective

English

If f is monotone and injective, then f is strictly monotone.

Русский

Если f монотонна и инъективна, то f строго монотонна.

LaTeX

$$$$\\text{Monotone } f \\land \\text{Injective } f \\Rightarrow \\text{StrictMono } f.$$$$

Lean4

theorem strictMono_of_injective (h₁ : Monotone f) (h₂ : Injective f) : StrictMono f := fun _ _ h ↦
  (h₁ h.le).lt_of_ne fun H ↦ h.ne <| h₂ H

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

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

Разделы

Аффилиация

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