circleMap_notMem_ball — Mathlib

English

The image circleMap c R θ lies on the circle with center c and radius |R|, hence it is not contained in the open ball B(c,R).

Русский

Изображение circleMap c R θ лежит на окружности с центром в c и радиусом |R|, следовательно не принадлежит открытому шару B(c,R).

LaTeX

$$$ circleMap c R θ \notin B(c,R) $$$

Lean4

theorem circleMap_notMem_ball (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ ∉ ball c R := by
  simp [Complex.dist_eq, le_abs_self]

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