continuous_circleMap

Mathlib.MeasureTheory.Integral.CircleIntegral

URI: https://scilib.ai/kg/mathlib#continuous_circleMap

English

The circle map c R is continuous as a function of θ.

Русский

Круговая карта c R непрерывна как функция от θ.

LaTeX

$$$ circleMap(c,R): \mathbb{R} \to \mathbb{C} \text{ is continuous}. $$$

Lean4

@[continuity, fun_prop]
theorem continuous_circleMap (c : ℂ) (R : ℝ) : Continuous (circleMap c R) :=
  (differentiable_circleMap c R).continuous

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

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

Разделы

Аффилиация

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