coe_tanPartialHomeomorph

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

The underlying map of the partial homeomorphism tanPartialHomeomorph is the tangent function.

Русский

Подлежащая функция частичного гомеоморфизма tanPartialHomeomorph совпадает с функцией тангенса.

LaTeX

$$$ \forall x, \ anPartialHomeomorph(x) = \tan x.$$$

Lean4

@[simp]
theorem coe_tanPartialHomeomorph : ⇑tanPartialHomeomorph = tan :=
  rfl

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

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

Разделы

Аффилиация

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