circleMap_ne_center

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

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

English

If R ≠ 0, circleMap c R θ is never equal to the center c.

Русский

Если R ≠ 0, circleMap c R θ никогда не равно центру c.

LaTeX

$$$ R \neq 0 \Rightarrow circleMap c R θ \neq c $$$

Lean4

theorem circleMap_ne_center {c : ℂ} {R : ℝ} (hR : R ≠ 0) {θ : ℝ} : circleMap c R θ ≠ c :=
  mt circleMap_eq_center_iff.1 hR

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

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

Разделы

Аффилиация

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