---

Step * 1 of Lemma weak-continuity-skolem_functionality


1. [T] : Type
2. [S] : Type
3. i : T ⟶ S
4. e1 : Bij(T;S;i)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : (ℕ ⟶ T) ⟶ ℕ
7. ∀f,g:ℕ ⟶ T.  ((f = g ∈ (ℕM f ⟶ T)) ⇒ (((λf@0.(F (i o f@0))) f) = ((λf@0.(F (i o f@0))) g) ∈ ℕ))
8. j : S ⟶ T
9. ∀b:S. ((i (j b)) = b ∈ S)
10. ∀a:T. ((j (i a)) = a ∈ T)
⊢ weak-continuity-skolem(S;F)
BY
{ (D 0 With ⌜λf.(M (j o f))⌝  THEN Auto THEN Reduce 0) }

1
1. T : Type
2. S : Type
3. i : T ⟶ S
4. e1 : Bij(T;S;i)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : (ℕ ⟶ T) ⟶ ℕ
7. ∀f,g:ℕ ⟶ T.  ((f = g ∈ (ℕM f ⟶ T)) ⇒ (((λf@0.(F (i o f@0))) f) = ((λf@0.(F (i o f@0))) g) ∈ ℕ))
8. j : S ⟶ T
9. ∀b:S. ((i (j b)) = b ∈ S)
10. ∀a:T. ((j (i a)) = a ∈ T)
11. f : ℕ ⟶ S
12. g : ℕ ⟶ S
13. f = g ∈ (ℕ(λf.(M (j o f))) f ⟶ S)
⊢ (F f) = (F g) ∈ ℕ

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [S]  :  Type
3.  i  :  T  {}\mrightarrow{}  S
4.  e1  :  Bij(T;S;i)
5.  F  :  (\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}
6.  M  :  (\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  T.    ((f  =  g)  {}\mRightarrow{}  (((\mlambda{}f@0.(F  (i  o  f@0)))  f)  =  ((\mlambda{}f@0.(F  (i  o  f@0)))  g)))
8.  j  :  S  {}\mrightarrow{}  T
9.  \mforall{}b:S.  ((i  (j  b))  =  b)
10.  \mforall{}a:T.  ((j  (i  a))  =  a)
\mvdash{}  weak-continuity-skolem(S;F)


By

---

Latex:
(D  0  With  \mkleeneopen{}\mlambda{}f.(M  (j  o  f))\mkleeneclose{}    THEN  Auto  THEN  Reduce  0)

---

Home Index