---

Step * 1 2 of Lemma extend-face-term-uniqueness


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
8. b ≤ phi
9. ∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((a)<g> = u(g) ∈ Point(face_lattice(I)))
10. ∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((b)<g> = u(g) ∈ Point(face_lattice(I)))
11. Refl(Point(face_lattice(I));x,y.x ≤ y)
12. Trans(Point(face_lattice(I));x,y.x ≤ y)
13. ∀x,y:Point(face_lattice(I)).  (x ≤ y ⇒ y ≤ x ⇒ (x = y ∈ Point(face_lattice(I))))
14. f : I ⟶ I
15. (b)<f> = 1 ∈ Point(face_lattice(I))
⊢ (a)<f> = 1 ∈ Point(face_lattice(I))
BY
{ ((Assert (b)<f> ≤ (phi)<f> BY
          (BLemma `lattice-hom-le` THEN Auto))
   THEN (RWO "-2" (-1) THENA Auto)
   THEN (RWO "lattice-1-le-iff" (-1) THENA Auto)
   THEN (Assert (phi f) = 1 BY
               (UnfoldTopAb 0 THEN 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
8. b ≤ phi
9. ∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((a)<g> = u(g) ∈ Point(face_lattice(I)))
10. ∀[g:{f:I ⟶ I| (phi f) = 1} ]. ((b)<g> = u(g) ∈ Point(face_lattice(I)))
11. Refl(Point(face_lattice(I));x,y.x ≤ y)
12. Trans(Point(face_lattice(I));x,y.x ≤ y)
13. ∀x,y:Point(face_lattice(I)).  (x ≤ y ⇒ y ≤ x ⇒ (x = y ∈ Point(face_lattice(I))))
14. f : I ⟶ I
15. (b)<f> = 1 ∈ Point(face_lattice(I))
16. (phi)<f> = 1 ∈ Point(face_lattice(I))
17. (phi f) = 1
⊢ (a)<f> = 1 ∈ Point(face_lattice(I))

---

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.  b  :  Point(face\_lattice(I))
6.  I,phi(I)  \mequiv{}  \{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\} 
7.  a  \mleq{}  phi
8.  b  \mleq{}  phi
9.  \mforall{}[g:\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  ].  ((a)<g>  =  u(g))
10.  \mforall{}[g:\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  ].  ((b)<g>  =  u(g))
11.  Refl(Point(face\_lattice(I));x,y.x  \mleq{}  y)
12.  Trans(Point(face\_lattice(I));x,y.x  \mleq{}  y)
13.  \mforall{}x,y:Point(face\_lattice(I)).    (x  \mleq{}  y  {}\mRightarrow{}  y  \mleq{}  x  {}\mRightarrow{}  (x  =  y))
14.  f  :  I  {}\mrightarrow{}  I
15.  (b)<f>  =  1
\mvdash{}  (a)<f>  =  1


By

---

Latex:
((Assert  (b)<f>  \mleq{}  (phi)<f>  BY
                (BLemma  `lattice-hom-le`  THEN  Auto))
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  (RWO  "lattice-1-le-iff"  (-1)  THENA  Auto)
  THEN  (Assert  (phi  f)  =  1  BY
                          (UnfoldTopAb  0  THEN  Auto)))

---

Home Index