---

Step * of Lemma fl_all-join

∀[I:fset(ℕ)]. ∀[i:ℕ]. ∀[a,b:Point(face_lattice(I+i))].  ((∀i.a ∨ b) = (∀i.a) ∨ (∀i.b) ∈ Point(face_lattice(I)))
BY
{ ((Auto THEN Unfold `fl_all` 0)
   THEN (GenConcl ⌜fl-all-hom(I;i) = h ∈ Hom(face_lattice(I+i);face_lattice(I))⌝⋅
         THENA (InstLemma `fl-all-hom_wf1` [⌜I⌝;⌜i⌝]⋅ THEN Auto)
         )
   THEN Thin (-1)
   THEN DVar `h'
   THEN Auto
   THEN RWO "-1.2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].  \mforall{}[a,b:Point(face\_lattice(I+i))].    ((\mforall{}i.a  \mvee{}  b)  =  (\mforall{}i.a)  \mvee{}  (\mforall{}i.b))


By

---

Latex:
((Auto  THEN  Unfold  `fl\_all`  0)
  THEN  (GenConcl  \mkleeneopen{}fl-all-hom(I;i)  =  h\mkleeneclose{}\mcdot{}  THENA  (InstLemma  `fl-all-hom\_wf1`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  Thin  (-1)
  THEN  DVar  `h'
  THEN  Auto
  THEN  RWO  "-1.2"  0
  THEN  Auto)

---

Home Index