Step
*
1
1
1
1
1
1
1
1
1
of Lemma
mcompact-stable-union
1. X : Type
2. d : metric(X)
3. T : Type
4. P : T ⟶ X ⟶ ℙ
5. ∀i:T. ∀x,y:X. (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
6. finite(T)
7. mcomplete(X with d)
8. ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. mcomplete(stable-union(X;T;i,x.P[i;x]) with d)
10. t : T
11. ∀i:T. m-TB({x:X| P[i;x]} ;d)
12. k : ℕ
13. sz : i:T ⟶ ℕ+
14. pts : i:T ⟶ ℕsz i ⟶ {x:X| P[i;x]}
15. ∀i:T. ∀x:{x:X| P[i;x]} . ∃i1:ℕsz i. (mdist(d;x;pts i i1) ≤ (r1/r((2 * (k + 1)) + 1)))
16. n : ℕ
17. i:T × ℕsz i ~ ℕn
18. f : ℕn ⟶ (i:T × ℕsz i)
19. Bij(ℕn;i:T × ℕsz i;f)
20. 0 < n
21. λj.let i,a = f j
in pts i a ∈ ℕn ⟶ stable-union(X;T;i,x.P[i;x])
22. x : X
23. i : T
24. P[i;x]
25. ∀i:ℕn
(((r1/r((2 * (k + 1)) + 1)) < mdist(d;x;(λj.let i,a = f j in pts i a) i))
∨ (mdist(d;x;(λj.let i,a = f j in pts i a) i) < (r1/r(k + 1))))
26. ∀i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) i) ∈ ℝ)
27. i1 : ℕsz i
28. mdist(d;x;pts i i1) ≤ (r1/r((2 * (k + 1)) + 1))
29. j : ℕn
30. (f j) = <i, i1> ∈ (i:T × ℕsz i)
31. (r1/r((2 * (k + 1)) + 1)) < mdist(d;x;let i,a = f j
in pts i a)
⊢ False
BY
{ ((Assert let i,a = f j in pts i a = (pts i i1) ∈ {x:X| P[i;x]} BY
(RWO "-2" 0 THEN Reduce 0 THEN Auto))
THEN (RWO "-1" (-2) THENA Auto)
) }
1
1. X : Type
2. d : metric(X)
3. T : Type
4. P : T ⟶ X ⟶ ℙ
5. ∀i:T. ∀x,y:X. (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
6. finite(T)
7. mcomplete(X with d)
8. ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. mcomplete(stable-union(X;T;i,x.P[i;x]) with d)
10. t : T
11. ∀i:T. m-TB({x:X| P[i;x]} ;d)
12. k : ℕ
13. sz : i:T ⟶ ℕ+
14. pts : i:T ⟶ ℕsz i ⟶ {x:X| P[i;x]}
15. ∀i:T. ∀x:{x:X| P[i;x]} . ∃i1:ℕsz i. (mdist(d;x;pts i i1) ≤ (r1/r((2 * (k + 1)) + 1)))
16. n : ℕ
17. i:T × ℕsz i ~ ℕn
18. f : ℕn ⟶ (i:T × ℕsz i)
19. Bij(ℕn;i:T × ℕsz i;f)
20. 0 < n
21. λj.let i,a = f j
in pts i a ∈ ℕn ⟶ stable-union(X;T;i,x.P[i;x])
22. x : X
23. i : T
24. P[i;x]
25. ∀i:ℕn
(((r1/r((2 * (k + 1)) + 1)) < mdist(d;x;(λj.let i,a = f j in pts i a) i))
∨ (mdist(d;x;(λj.let i,a = f j in pts i a) i) < (r1/r(k + 1))))
26. ∀i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) i) ∈ ℝ)
27. i1 : ℕsz i
28. mdist(d;x;pts i i1) ≤ (r1/r((2 * (k + 1)) + 1))
29. j : ℕn
30. (f j) = <i, i1> ∈ (i:T × ℕsz i)
31. (r1/r((2 * (k + 1)) + 1)) < mdist(d;x;pts i i1)
32. let i,a = f j in pts i a = (pts i i1) ∈ {x:X| P[i;x]}
⊢ False
Latex:
Latex:
1. X : Type
2. d : metric(X)
3. T : Type
4. P : T {}\mrightarrow{} X {}\mrightarrow{} \mBbbP{}
5. \mforall{}i:T. \mforall{}x,y:X. (P[i;x] {}\mRightarrow{} y \mequiv{} x {}\mRightarrow{} P[i;y])
6. finite(T)
7. mcomplete(X with d)
8. \mforall{}i:T. mcompact(\{x:X| P[i;x]\} ;d)
9. mcomplete(stable-union(X;T;i,x.P[i;x]) with d)
10. t : T
11. \mforall{}i:T. m-TB(\{x:X| P[i;x]\} ;d)
12. k : \mBbbN{}
13. sz : i:T {}\mrightarrow{} \mBbbN{}\msupplus{}
14. pts : i:T {}\mrightarrow{} \mBbbN{}sz i {}\mrightarrow{} \{x:X| P[i;x]\}
15. \mforall{}i:T. \mforall{}x:\{x:X| P[i;x]\} . \mexists{}i1:\mBbbN{}sz i. (mdist(d;x;pts i i1) \mleq{} (r1/r((2 * (k + 1)) + 1)))
16. n : \mBbbN{}
17. i:T \mtimes{} \mBbbN{}sz i \msim{} \mBbbN{}n
18. f : \mBbbN{}n {}\mrightarrow{} (i:T \mtimes{} \mBbbN{}sz i)
19. Bij(\mBbbN{}n;i:T \mtimes{} \mBbbN{}sz i;f)
20. 0 < n
21. \mlambda{}j.let i,a = f j
in pts i a \mmember{} \mBbbN{}n {}\mrightarrow{} stable-union(X;T;i,x.P[i;x])
22. x : X
23. i : T
24. P[i;x]
25. \mforall{}i:\mBbbN{}n
(((r1/r((2 * (k + 1)) + 1)) < mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i))
\mvee{} (mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i) < (r1/r(k + 1))))
26. \mforall{}i:\mBbbN{}n. (mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i) \mmember{} \mBbbR{})
27. i1 : \mBbbN{}sz i
28. mdist(d;x;pts i i1) \mleq{} (r1/r((2 * (k + 1)) + 1))
29. j : \mBbbN{}n
30. (f j) = <i, i1>
31. (r1/r((2 * (k + 1)) + 1)) < mdist(d;x;let i,a = f j
in pts i a)
\mvdash{} False
By
Latex:
((Assert let i,a = f j in pts i a = (pts i i1) BY
(RWO "-2" 0 THEN Reduce 0 THEN Auto))
THEN (RWO "-1" (-2) THENA Auto)
)
Home
Index