circleMap_mem_sphere — Mathlib

English

If radius is nonnegative, circleMap c R θ lies on the sphere with center c and radius R.

Русский

Если радиус неотрицателен, circleMap c R θ лежит на сфере с центром в c и радиусом R.

LaTeX

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

Lean4

theorem circleMap_mem_sphere (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ sphere c R := by
  simpa only [abs_of_nonneg hR] using circleMap_mem_sphere' c R θ

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