continuous_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

The function arctan is continuous on ℝ.

Русский

Функция arctan непрерывна на всей сфере ℝ.

LaTeX

$$$\\\\operatorname{Continuous}(\\\\arctan): \\\\mathbb{R} \\\\to \\\\mathbb{R}$.$$

Lean4

@[continuity]
theorem continuous_arctan : Continuous arctan :=
  continuous_subtype_val.comp tanOrderIso.toHomeomorph.continuous_invFun

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

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

Разделы

Аффилиация

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