injOn

Mathlib.Order.Monotone.Basic

URI: https://scilib.ai/kg/mathlib#StrictMonoOn.injOn

English

If f is strictly monotone on S, then f is injective on S.

Русский

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

LaTeX

$$$ (hf : StrictMonoOn f s) : s.InjOn f $$$

Lean4

theorem injOn (hf : StrictMonoOn f s) : s.InjOn f := fun x hx y hy hxy ↦
  show Ordering.eq.Compares x y from (hf.compares hx hy).1 hxy

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

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

Разделы

Аффилиация

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