sinOrderIso_apply

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

For all x in the domain, sinOrderIso x = ⟨ sin x, sin_mem_Icc x ⟩.

Русский

Для всех x в области определения, sinOrderIso x = ⟨ sin x, sin_mem_Icc x ⟩.

LaTeX

$$$\\\\sinOrderIso x = \\\\langle \\\\sin x, \\\\sin\\\\_mem\\\\_Icc x \\\\rangle$$$

Lean4

theorem sinOrderIso_apply (x : Icc (-(π / 2)) (π / 2)) : sinOrderIso x = ⟨sin x, sin_mem_Icc x⟩ :=
  rfl

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

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

Разделы

Аффилиация

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