circleMap_mem_sphere'

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

URI: https://scilib.ai/kg/mathlib#circleMap_mem_sphere'

English

For any c ∈ ℂ, R ∈ ℝ, θ ∈ ℝ, circleMap c R θ lies on the sphere with center c and radius |R|.

Русский

Для любых c ∈ ℂ, R ∈ ℝ и θ ∈ ℝ circleMap c R θ принадлежит сфере с центром в c и радиусом |R|.

LaTeX

$$$ circleMap c R θ \in sphere c |R| $$$

Lean4

theorem circleMap_mem_sphere' (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ ∈ sphere c |R| := by simp

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

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

Разделы

Аффилиация

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