---

Step * 4 1 2 1 1 of Lemma general-uniform-continuity-from-fan


1. B : ℕ ⟶ Type
2. ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. T : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. ∀f:i:ℕ ⟶ (B i)
     ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. k : ℕ
9. ∀f:i:ℕ ⟶ (B i). ∃n:ℕk. (↑isl(M n f))
10. 0 < k
11. f : i:ℕ ⟶ (B i)
12. g : i:ℕ ⟶ (B i)
13. f = g ∈ (i:ℕk - 1 ⟶ (B i))
14. n : ℕ
15. (M n f) = (inl (F f)) ∈ (T?)
16. ∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)
17. n1 : ℕ
18. (M n1 g) = (inl (F g)) ∈ (T?)
19. ∀n:ℕ. (M n g) = (inl (F g)) ∈ (T?) supposing ↑isl(M n g)
20. n3 : ℕk
21. ↑isl(M n3 f)
22. n2 : ℕk
23. ↑isl(M n2 g)
⊢ (F f) = (F g) ∈ T
BY
{ ((Assert ⌜(M n3 f) = (M n3 g) ∈ (T?)⌝⋅ THENA Auto) THEN (Assert ⌜(M n2 f) = (M n2 g) ∈ (T?)⌝⋅ THENA Auto)) }

1
1. B : ℕ ⟶ Type
2. ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. T : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. ∀f:i:ℕ ⟶ (B i)
     ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. k : ℕ
9. ∀f:i:ℕ ⟶ (B i). ∃n:ℕk. (↑isl(M n f))
10. 0 < k
11. f : i:ℕ ⟶ (B i)
12. g : i:ℕ ⟶ (B i)
13. f = g ∈ (i:ℕk - 1 ⟶ (B i))
14. n : ℕ
15. (M n f) = (inl (F f)) ∈ (T?)
16. ∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)
17. n1 : ℕ
18. (M n1 g) = (inl (F g)) ∈ (T?)
19. ∀n:ℕ. (M n g) = (inl (F g)) ∈ (T?) supposing ↑isl(M n g)
20. n3 : ℕk
21. ↑isl(M n3 f)
22. n2 : ℕk
23. ↑isl(M n2 g)
24. (M n3 f) = (M n3 g) ∈ (T?)
25. (M n2 f) = (M n2 g) ∈ (T?)
⊢ (F f) = (F g) ∈ T

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  Type
2.  \mforall{}i:\mBbbN{}.  (B  i)
3.  \mforall{}i:\mBbbN{}.  \mforall{}K:(B  i)  {}\mrightarrow{}  \mBbbN{}.    (\mexists{}Bnd:\mBbbN{}  [(\mforall{}t:B  i.  ((K  t)  \mleq{}  Bnd))])
4.  T  :  Type
5.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  (B  i))  {}\mrightarrow{}  T
6.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  (B  i))  {}\mrightarrow{}  (T?)
7.  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  (B  i)
          ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))  \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f)))
8.  k  :  \mBbbN{}
9.  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  (B  i).  \mexists{}n:\mBbbN{}k.  (\muparrow{}isl(M  n  f))
10.  0  <  k
11.  f  :  i:\mBbbN{}  {}\mrightarrow{}  (B  i)
12.  g  :  i:\mBbbN{}  {}\mrightarrow{}  (B  i)
13.  f  =  g
14.  n  :  \mBbbN{}
15.  (M  n  f)  =  (inl  (F  f))
16.  \mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f)
17.  n1  :  \mBbbN{}
18.  (M  n1  g)  =  (inl  (F  g))
19.  \mforall{}n:\mBbbN{}.  (M  n  g)  =  (inl  (F  g))  supposing  \muparrow{}isl(M  n  g)
20.  n3  :  \mBbbN{}k
21.  \muparrow{}isl(M  n3  f)
22.  n2  :  \mBbbN{}k
23.  \muparrow{}isl(M  n2  g)
\mvdash{}  (F  f)  =  (F  g)


By

---

Latex:
((Assert  \mkleeneopen{}(M  n3  f)  =  (M  n3  g)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Assert  \mkleeneopen{}(M  n2  f)  =  (M  n2  g)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index