arcsin_le_arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

If x ≤ y then arcsin x ≤ arcsin y.

Русский

Если x ≤ y, то arcsin x ≤ arcsin y.

LaTeX

$$$x \le y \Rightarrow \\arcsin x \le \\arcsin y$$$

Lean4

@[gcongr]
theorem arcsin_le_arcsin {x y : ℝ} (h : x ≤ y) : arcsin x ≤ arcsin y :=
  monotone_arcsin h

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

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

Разделы

Аффилиация

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