---

Step * 1 of Lemma extend-face-term-unique


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))))
BY
{ Auto }

---

Latex:

---

Latex:

1.  [I]  :  fset(\mBbbN{})
2.  [phi]  :  Point(face\_lattice(I))
3.  [u]  :  \{I,phi  \mvdash{}  \_:\mBbbF{}\}
4.  [a]  :  Point(face\_lattice(I))
5.  \mforall{}[b:Point(face\_lattice(I))]
          a  =  b 
          supposing  a  \mleq{}  phi
          \mwedge{}  b  \mleq{}  phi
          \mwedge{}  (\mforall{}[g:\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  ].  ((a)<g>  =  u(g)))
          \mwedge{}  (\mforall{}[g:\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  ].  ((b)<g>  =  u(g)))
\mvdash{}  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:
Auto

---

Home Index