---

Step * 1 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
∧ 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))
BY
{ ((InstLemma `lattice-le-order` [⌜face_lattice(I)⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN BackThruHyp' (-1)
   THEN Auto
   THEN BLemma `face_lattice-le`
   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. (a)<f> = 1 ∈ Point(face_lattice(I))
⊢ (b)<f> = 1 ∈ Point(face_lattice(I))

2
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))

---

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
\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  =  b


By

---

Latex:
((InstLemma  `lattice-le-order`  [\mkleeneopen{}face\_lattice(I)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  BackThruHyp'  (-1)
  THEN  Auto
  THEN  BLemma  `face\_lattice-le`
  THEN  Auto)

---

Home Index