---

Step * of Lemma dM-hom-invariant

∀[I:fset(ℕ)]. ∀[J:{J:fset(ℕ)| I ⊆ J} ]. ∀[h:Hom(dM(J);dM(I))].
  ∀[x:Point(dM(I))]. ((h x) = x ∈ Point(dM(I))) 
  supposing ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
BY
{ (Auto
   THEN (InstLemma `dM-hom-basis` [⌜J⌝;⌜x⌝;⌜dM(I)⌝;⌜free-dml-deq(names(I);NamesDeq)⌝;⌜h⌝]⋅
         THENA (Auto
                THEN (Subst' Point(dM(I)) ~ Point(free-DeMorgan-lattice(names(I);NamesDeq)) 0 THENM Auto)
                THEN (RWO "dM-point" 0 THENA Auto)
                THEN RepUR ``free-DeMorgan-lattice`` 0
                THEN RWO "free-dl-point" 0
                THEN Auto)
         )
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Thin (-1)
   THEN (InstLemma  `dM-basis` [⌜I⌝;⌜x⌝]⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Thin (-1)) }

1
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
5. x : Point(dM(I))
⊢ \/(λs./\(λx.(h free-dl-inc(x))"(s))"(x)) = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(dM(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[J:\{J:fset(\mBbbN{})|  I  \msubseteq{}  J\}  ].  \mforall{}[h:Hom(dM(J);dM(I))].
    \mforall{}[x:Point(dM(I))].  ((h  x)  =  x)  supposing  \mforall{}i:names(I).  (((h  <i>)  =  <i>)  \mwedge{}  ((h  ə-i>)  =  ə-i>))


By

---

Latex:
(Auto
  THEN  (InstLemma  `dM-hom-basis`  [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}dM(I)\mkleeneclose{};\mkleeneopen{}free-dml-deq(names(I);NamesDeq)\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  (Subst'  Point(dM(I))  \msim{}  Point(free-DeMorgan-lattice(names(I);NamesDeq))  0
                            THENM  Auto
                            )
                            THEN  (RWO  "dM-point"  0  THENA  Auto)
                            THEN  RepUR  ``free-DeMorgan-lattice``  0
                            THEN  RWO  "free-dl-point"  0
                            THEN  Auto)
              )
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Thin  (-1)
  THEN  (InstLemma    `dM-basis`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Thin  (-1))

---

Home Index