---

Step * of Lemma extend-face-term-unique

∀[I:fset(ℕ)]. ∀[phi:Point(face_lattice(I))]. ∀[u:{I,phi ⊢ _:𝔽}]. ∀[a:Point(face_lattice(I))].
  a = extend-face-term(I;phi;u) ∈ Point(face_lattice(I)) 
  supposing a ≤ phi ∧ (∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((a)<g> = u(g) ∈ Point(face_lattice(I))))
BY
{ (InstLemma `extend-face-term-uniqueness` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. [I] : fset(ℕ)
2. [phi] : Point(face_lattice(I))
3. [u] : {I,phi ⊢ _:𝔽}
4. [a] : Point(face_lattice(I))
5. ∀[b:Point(face_lattice(I))]
     a = b ∈ Point(face_lattice(I)) 
     supposing a ≤ phi
     ∧ b ≤ phi
     ∧ (∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((a)<g> = u(g) ∈ Point(face_lattice(I))))
     ∧ (∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((b)<g> = u(g) ∈ Point(face_lattice(I))))
⊢ a = extend-face-term(I;phi;u) ∈ Point(face_lattice(I)) 
  supposing a ≤ phi ∧ (∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((a)<g> = u(g) ∈ Point(face_lattice(I))))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:Point(face\_lattice(I))].  \mforall{}[u:\{I,phi  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[a:Point(face\_lattice(I))].
    a  =  extend-face-term(I;phi;u)  supposing  a  \mleq{}  phi  \mwedge{}  (\mforall{}[g:\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  ].  ((a)<g>  =  u(g)))


By

---

Latex:
(InstLemma  `extend-face-term-uniqueness`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index