Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sph Structured version   Visualization version   GIF version

Definition df-sph 45083
Description: Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 22921, or even in any extended structure having a base set and a distance function into the real numbers. (Contributed by AV, 14-Jan-2023.)
Assertion
Ref Expression
df-sph Sphere = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))
Distinct variable group:   𝑟,𝑝,𝑤,𝑥

Detailed syntax breakdown of Definition df-sph
StepHypRef Expression
1 csph 45081 . 2 class Sphere
2 vw . . 3 setvar 𝑤
3 cvv 3469 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vr . . . 4 setvar 𝑟
62cv 1537 . . . . 5 class 𝑤
7 cbs 16474 . . . . 5 class Base
86, 7cfv 6334 . . . 4 class (Base‘𝑤)
9 cc0 10526 . . . . 5 class 0
10 cpnf 10661 . . . . 5 class +∞
11 cicc 12729 . . . . 5 class [,]
129, 10, 11co 7140 . . . 4 class (0[,]+∞)
13 vp . . . . . . . 8 setvar 𝑝
1413cv 1537 . . . . . . 7 class 𝑝
154cv 1537 . . . . . . 7 class 𝑥
16 cds 16565 . . . . . . . 8 class dist
176, 16cfv 6334 . . . . . . 7 class (dist‘𝑤)
1814, 15, 17co 7140 . . . . . 6 class (𝑝(dist‘𝑤)𝑥)
195cv 1537 . . . . . 6 class 𝑟
2018, 19wceq 1538 . . . . 5 wff (𝑝(dist‘𝑤)𝑥) = 𝑟
2120, 13, 8crab 3134 . . . 4 class {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}
224, 5, 8, 12, 21cmpo 7142 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟})
232, 3, 22cmpt 5122 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))
241, 23wceq 1538 1 wff Sphere = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))
Colors of variables: wff setvar class
This definition is referenced by:  spheres  45099
  Copyright terms: Public domain W3C validator