Step
*
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. P[i;x])
24. ∀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))))
25. ∀i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) i) ∈ ℝ)
⊢ ∃i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) i) ≤ (r1/r(k + 1)))
BY
{ ((InstLemma `int_seg-case`
[⌜0⌝;⌜n⌝;⌜λ2i.mdist(d;x;(λj.let i,a = f j in pts i a) i) < (r1/r(k + 1))⌝;
⌜λ2i.(r1/r((2 * (k + 1)) + 1)) < mdist(d;x;(λj.let i,a = f j in pts i a) i)⌝]⋅
THENA (Auto THEN RenameVar `j' (-1) THEN (D -3 With ⌜j⌝ THENM D -1) THEN Auto)
)
THEN D -1
THEN Try ((ParallelLast THEN 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. P[i;x])
24. ∀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))))
25. ∀i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) i) ∈ ℝ)
26. ∀k@0:ℕn. ((r1/r((2 * (k + 1)) + 1)) < mdist(d;x;(λj.let i,a = f j in pts i a) k@0))
⊢ ∃i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) i) ≤ (r1/r(k + 1)))
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. \mneg{}\mneg{}(\mexists{}i:T. P[i;x])
24. \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))))
25. \mforall{}i:\mBbbN{}n. (mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i) \mmember{} \mBbbR{})
\mvdash{} \mexists{}i:\mBbbN{}n. (mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i) \mleq{} (r1/r(k + 1)))
By
Latex:
((InstLemma `int\_seg-case`
[\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i) < (r1/r(k + 1))\mkleeneclose{};
\mkleeneopen{}\mlambda{}\msubtwo{}i.(r1/r((2 * (k + 1)) + 1)) < mdist(d;x;(\mlambda{}j.let i,a = f j in pts i a) i)\mkleeneclose{}]\mcdot{}
THENA (Auto THEN RenameVar `j' (-1) THEN (D -3 With \mkleeneopen{}j\mkleeneclose{} THENM D -1) THEN Auto)
)
THEN D -1
THEN Try ((ParallelLast THEN Auto)))
Home
Index