circleMap_ne_mem_ball

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

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

← MathLib Explorer

English

If w ∈ B(c,R), then circleMap c R θ ≠ w for every θ.

Русский

Если w ∈ B(c,R), то circleMap c R θ ≠ w при любом θ.

LaTeX

$$$ w \in B(c,R) \Rightarrow \forall \theta,\; circleMap c R \theta \neq w $$$

Lean4

theorem circleMap_ne_mem_ball {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ ball c R) (θ : ℝ) : circleMap c R θ ≠ w :=
  (ne_of_mem_of_not_mem hw (circleMap_notMem_ball _ _ _)).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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