dist_center_eq_dist_center_of_mem_sphere'

English

Same as above, distance equality from center for any two points in the same sphere.

Русский

То же самое: расстояния до центра для любых двух точек на одной сфере равны.

LaTeX

$$$$ hp_1 : p_1 \in s \land 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 s.center p₁ = dist s.center p₂ := by rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]

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