Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-totbnd Structured version   Visualization version   GIF version

Definition df-totbnd 36636
Description: Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-totbnd TotBnd = (π‘₯ ∈ V ↦ {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))})
Distinct variable group:   𝑏,𝑑,π‘š,𝑣,π‘₯,𝑦

Detailed syntax breakdown of Definition df-totbnd
StepHypRef Expression
1 ctotbnd 36634 . 2 class TotBnd
2 vx . . 3 setvar π‘₯
3 cvv 3475 . . 3 class V
4 vv . . . . . . . . . 10 setvar 𝑣
54cv 1541 . . . . . . . . 9 class 𝑣
65cuni 4909 . . . . . . . 8 class βˆͺ 𝑣
72cv 1541 . . . . . . . 8 class π‘₯
86, 7wceq 1542 . . . . . . 7 wff βˆͺ 𝑣 = π‘₯
9 vb . . . . . . . . . . 11 setvar 𝑏
109cv 1541 . . . . . . . . . 10 class 𝑏
11 vy . . . . . . . . . . . 12 setvar 𝑦
1211cv 1541 . . . . . . . . . . 11 class 𝑦
13 vd . . . . . . . . . . . 12 setvar 𝑑
1413cv 1541 . . . . . . . . . . 11 class 𝑑
15 vm . . . . . . . . . . . . 13 setvar π‘š
1615cv 1541 . . . . . . . . . . . 12 class π‘š
17 cbl 20931 . . . . . . . . . . . 12 class ball
1816, 17cfv 6544 . . . . . . . . . . 11 class (ballβ€˜π‘š)
1912, 14, 18co 7409 . . . . . . . . . 10 class (𝑦(ballβ€˜π‘š)𝑑)
2010, 19wceq 1542 . . . . . . . . 9 wff 𝑏 = (𝑦(ballβ€˜π‘š)𝑑)
2120, 11, 7wrex 3071 . . . . . . . 8 wff βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑)
2221, 9, 5wral 3062 . . . . . . 7 wff βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑)
238, 22wa 397 . . . . . 6 wff (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))
24 cfn 8939 . . . . . 6 class Fin
2523, 4, 24wrex 3071 . . . . 5 wff βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))
26 crp 12974 . . . . 5 class ℝ+
2725, 13, 26wral 3062 . . . 4 wff βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))
28 cmet 20930 . . . . 5 class Met
297, 28cfv 6544 . . . 4 class (Metβ€˜π‘₯)
3027, 15, 29crab 3433 . . 3 class {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))}
312, 3, 30cmpt 5232 . 2 class (π‘₯ ∈ V ↦ {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))})
321, 31wceq 1542 1 wff TotBnd = (π‘₯ ∈ V ↦ {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))})
Colors of variables: wff setvar class
This definition is referenced by:  istotbnd  36637
  Copyright terms: Public domain W3C validator