dist_of_mem_subset_sphere — Mathlib

English

If p ∈ ps and ps ⊆ s, then dist(p, s.center) = s.radius.

Русский

Если p ∈ ps и ps ⊆ s, то dist(p, s.center) = s.radius.

LaTeX

$$$$ (p \in ps) \Rightarrow (ps \subseteq s) \Rightarrow \operatorname{dist}(p, s.center) = s.radius. $$$$

Lean4

theorem dist_of_mem_subset_sphere {p : P} {ps : Set P} {s : Sphere P} (hp : p ∈ ps) (hps : ps ⊆ (s : Set P)) :
    dist p s.center = s.radius :=
  mem_sphere.1 (Sphere.mem_coe.1 (Set.mem_of_mem_of_subset hp hps))

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