dist_of_mem_subset_mk_sphere — Mathlib

English

If ps ⊆ ↑(⟨c,r⟩ : Sphere P), then dist(p,c) = r for p ∈ ps.

Русский

Если ps ⊆ ↑(⟨c,r⟩ : Sphere P), тогда dist(p,c) = r для p ∈ ps.

LaTeX

$$$$ (p \in ps) \Rightarrow (ps \subseteq \uparrow(⟨c,r⟩ : Sphere P)) \Rightarrow \operatorname{dist}(p,c) = r. $$$$

Lean4

theorem dist_of_mem_subset_mk_sphere {p c : P} {ps : Set P} {r : ℝ} (hp : p ∈ ps) (hps : ps ⊆ ↑(⟨c, r⟩ : Sphere P)) :
    dist p c = r :=
  dist_of_mem_subset_sphere hp hps

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