---

Step * of Lemma fl-all-decomp

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[phi:Point(face-lattice(T;eq))]. ∀[i:T].
  (phi = (∀i.phi) ∨ phi ∧ (i=0) ∨ phi ∧ (i=1) ∈ Point(face-lattice(T;eq)))
BY
{ (Auto
   THEN (Assert AntiSym(Point(face-lattice(T;eq));x,y.x ≤ y) BY
               ((InstLemma `lattice-le-order` [⌜face-lattice(T;eq)⌝]⋅ THENM D -1) THEN Auto))
   THEN BackThruHyp' (-1)
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. phi : Point(face-lattice(T;eq))
4. i : T
5. ∀x,y:Point(face-lattice(T;eq)).  (x ≤ y ⇒ y ≤ x ⇒ (x = y ∈ Point(face-lattice(T;eq))))
⊢ phi ≤ (∀i.phi) ∨ phi ∧ (i=0) ∨ phi ∧ (i=1)

2
1. T : Type
2. eq : EqDecider(T)
3. phi : Point(face-lattice(T;eq))
4. i : T
5. ∀x,y:Point(face-lattice(T;eq)).  (x ≤ y ⇒ y ≤ x ⇒ (x = y ∈ Point(face-lattice(T;eq))))
⊢ (∀i.phi) ∨ phi ∧ (i=0) ∨ phi ∧ (i=1) ≤ phi

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[phi:Point(face-lattice(T;eq))].  \mforall{}[i:T].
    (phi  =  (\mforall{}i.phi)  \mvee{}  phi  \mwedge{}  (i=0)  \mvee{}  phi  \mwedge{}  (i=1))


By

---

Latex:
(Auto
  THEN  (Assert  AntiSym(Point(face-lattice(T;eq));x,y.x  \mleq{}  y)  BY
                          ((InstLemma  `lattice-le-order`  [\mkleeneopen{}face-lattice(T;eq)\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THEN  Auto))
  THEN  BackThruHyp'  (-1)
  THEN  Auto)

---

Home Index