dist_center_eq_dist_center_of_mem_sphere

English

If p1 and p2 lie on the same sphere, their distances to the center are equal.

Русский

Если точки p1 и p2 лежат на одной и той же сфере, их расстояния до центра равны.

LaTeX

$$$$ hp_1 : p_1 \in s \ Rightarrow hp_2 : p_2 \in s \Rightarrow dist(p_1, s.center) = dist(p_2, s.center). $$$$

Lean4

theorem dist_center_eq_dist_center_of_mem_sphere {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    dist p₁ s.center = dist p₂ s.center := by rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]

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