injOn

Mathlib.Order.Monotone.Basic

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

English

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

Русский

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

LaTeX

$$$ (hf : StrictAntiOn f s) \rightarrow s.InjOn f $$$

Lean4

theorem injOn (hf : StrictAntiOn f s) : s.InjOn f :=
  hf.dual_left.injOn

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

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

Разделы

Аффилиация

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