---

Step * 3 of Lemma interval-presheaf_wf


1. ∀x:fset(ℕ). (dM-lift(x;x;1) = (λx.x) ∈ (Point(dM(x)) ⟶ Point(dM(x))))
2. x : fset(ℕ)
3. y : fset(ℕ)
4. z : fset(ℕ)
5. f : y ⟶ x
6. g : z ⟶ y
⊢ ∀j:names(x). (((dM-lift(z;y;g) o dM-lift(y;x;f)) <j>) = (f ⋅ g j) ∈ Point(dM(z)))
BY
{ (Reduce 0 THEN (D 0 THENA Auto)) }

1
1. ∀x:fset(ℕ). (dM-lift(x;x;1) = (λx.x) ∈ (Point(dM(x)) ⟶ Point(dM(x))))
2. x : fset(ℕ)
3. y : fset(ℕ)
4. z : fset(ℕ)
5. f : y ⟶ x
6. g : z ⟶ y
7. j : names(x)
⊢ (dM-lift(z;y;g) (dM-lift(y;x;f) <j>)) = (f ⋅ g j) ∈ Point(dM(z))

---

Latex:

---

Latex:

1.  \mforall{}x:fset(\mBbbN{}).  (dM-lift(x;x;1)  =  (\mlambda{}x.x))
2.  x  :  fset(\mBbbN{})
3.  y  :  fset(\mBbbN{})
4.  z  :  fset(\mBbbN{})
5.  f  :  y  {}\mrightarrow{}  x
6.  g  :  z  {}\mrightarrow{}  y
\mvdash{}  \mforall{}j:names(x).  (((dM-lift(z;y;g)  o  dM-lift(y;x;f))  <j>)  =  (f  \mcdot{}  g  j))


By

---

Latex:
(Reduce  0  THEN  (D  0  THENA  Auto))

---

Home Index