---

Step * of Lemma extend-face-term-uniqueness

∀[I:fset(ℕ)]. ∀[phi:Point(face_lattice(I))]. ∀[u:{I,phi ⊢ _:𝔽}]. ∀[a,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))))
BY
{ (RepeatFor 5 (Intro)
   THEN (Assert I,phi(I) ≡ {f:I ⟶ I| (phi f) = 1}  BY
               (RepUR ``cubical-subset rep-sub-sheaf cat-arrow cube-cat`` 0 THEN D 0 THEN Auto))
   THEN (D 0 THENA (Auto THEN SubsumeC ⌜{f:I ⟶ I| (phi f) = 1} ⌝⋅ THEN Complete (Auto)))) }

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))
6. I,phi(I) ≡ {f:I ⟶ I| (phi f) = 1} 
7. 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 = b ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:Point(face\_lattice(I))].  \mforall{}[u:\{I,phi  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[a,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)))


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (Assert  I,phi(I)  \mequiv{}  \{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}    BY
                          (RepUR  ``cubical-subset  rep-sub-sheaf  cat-arrow  cube-cat``  0  THEN  D  0  THEN  Auto))
  THEN  (D  0  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  \mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))))

---

Home Index