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 43466
 Description: Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 22529, 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 43464 . 2 class Sphere
2 vw . . 3 setvar 𝑤
3 cvv 3398 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vr . . . 4 setvar 𝑟
62cv 1600 . . . . 5 class 𝑤
7 cbs 16255 . . . . 5 class Base
86, 7cfv 6135 . . . 4 class (Base‘𝑤)
9 cc0 10272 . . . . 5 class 0
10 cpnf 10408 . . . . 5 class +∞
11 cicc 12490 . . . . 5 class [,]
129, 10, 11co 6922 . . . 4 class (0[,]+∞)
13 vp . . . . . . . 8 setvar 𝑝
1413cv 1600 . . . . . . 7 class 𝑝
154cv 1600 . . . . . . 7 class 𝑥
16 cds 16347 . . . . . . . 8 class dist
176, 16cfv 6135 . . . . . . 7 class (dist‘𝑤)
1814, 15, 17co 6922 . . . . . 6 class (𝑝(dist‘𝑤)𝑥)
195cv 1600 . . . . . 6 class 𝑟
2018, 19wceq 1601 . . . . 5 wff (𝑝(dist‘𝑤)𝑥) = 𝑟
2120, 13, 8crab 3094 . . . 4 class {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}
224, 5, 8, 12, 21cmpt2 6924 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟})
232, 3, 22cmpt 4965 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))
241, 23wceq 1601 1 wff Sphere = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))
 Colors of variables: wff setvar class This definition is referenced by:  spheres  43482
 Copyright terms: Public domain W3C validator