---

Step * 1 of Lemma dM-to-FL-eq-1


1. I : fset(ℕ)
2. x : Point(dM(I))
3. dM-to-FL(I;x) = 1 ∈ Point(face_lattice(I))
⊢ x = 1 ∈ Point(dM(I))
BY
{ ((InstLemma `dM-hom-basis` [⌜I⌝; ⌜x⌝; ⌜face_lattice(I)⌝;⌜Deq(F(I))⌝;⌜λx.dM-to-FL(I;x)⌝]⋅
    THENA (Auto THEN (InstLemma `dM-to-FL-is-hom` [⌜I⌝]⋅ THENA Auto) THEN DoSubsume THEN Auto)
    )
   THEN Reduce -1
   THEN (Assert \/(λs./\(λx.dM-to-FL(I;free-dl-inc(x))"(s))"(x)) = 1 ∈ Point(face_lattice(I)) BY
               Auto)) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. dM-to-FL(I;x) = 1 ∈ Point(face_lattice(I))
4. dM-to-FL(I;x) = \/(λs./\(λx.dM-to-FL(I;free-dl-inc(x))"(s))"(x)) ∈ Point(face_lattice(I))
5. \/(λs./\(λx.dM-to-FL(I;free-dl-inc(x))"(s))"(x)) = 1 ∈ Point(face_lattice(I))
⊢ x = 1 ∈ Point(dM(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(dM(I))
3.  dM-to-FL(I;x)  =  1
\mvdash{}  x  =  1


By

---

Latex:
((InstLemma  `dM-hom-basis`  [\mkleeneopen{}I\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}face\_lattice(I)\mkleeneclose{};\mkleeneopen{}Deq(F(I))\mkleeneclose{};\mkleeneopen{}\mlambda{}x.dM-to-FL(I;x)\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  (InstLemma  `dM-to-FL-is-hom`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  DoSubsume  THEN  Auto)
    )
  THEN  Reduce  -1
  THEN  (Assert  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.dM-to-FL(I;free-dl-inc(x))"(s))"(x))  =  1  BY
                          Auto))

---

Home Index