coe_abs_toReal_of_sign_nonneg

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.coe_abs_toReal_of_sign_nonneg

← MathLib Explorer

English

If 0 ≤ θ.sign, then ↑|θ.toReal| = θ.

Русский

Если 0 ≤ θ.sign, то ↑|θ.toReal| = θ.

LaTeX

$$0 ≤ θ.sign ⇒ ↑|θ.toReal| = θ$$

Lean4

theorem coe_abs_toReal_of_sign_nonneg {θ : Angle} (h : 0 ≤ θ.sign) : ↑|θ.toReal| = θ := by
  rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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