injOn_sin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.injOn_sin

English

The sine function restricted to [-π/2, π/2] is injective.

Русский

Функция синуса, ограниченная на [-π/2, π/2], инъективна.

LaTeX

$$$\text{InjOn}(\sin, [-\\frac{\\pi}{2},\\frac{\\pi}{2}]).$$$

Lean4

theorem injOn_sin : InjOn sin (Icc (-(π / 2)) (π / 2)) :=
  strictMonoOn_sin.injOn

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

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

Разделы

Аффилиация

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