strictMono_iff_injective

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.strictMono_iff_injective

English

For a lift f, f is StrictMono if and only if f is Injective.

Русский

Для отображения-подъёма f: CircleDeg1Lift верно, что f строго монотонно тогда и только тогда, когда оно инъективно.

LaTeX

$$$\\text{StrictMono}(f) \\iff \\text{Injective}(f)$$$

Lean4

theorem strictMono_iff_injective : StrictMono f ↔ Injective f :=
  f.monotone.strictMono_iff_injective

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

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

Разделы

Аффилиация

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