Step * 5 of Lemma face_lattice-hom-fixes-sublattice2


1. fset(ℕ)
2. fset(ℕ)
3. J ⊆ I
4. Hom(face_lattice(I);face_lattice(J))
5. ∀i:names(J). (((f (i=0)) (i=0) ∈ Point(face_lattice(J))) ∧ ((f (i=1)) (i=1) ∈ Point(face_lattice(J))))
6. Point(face_lattice(J))
7. (f x) x ∈ Point(face_lattice(J))
8. names(J)
9. (f (i=0) ∧ x) (i=0) ∧ x ∈ Point(face_lattice(J))
⊢ (f (i=1) ∧ x) (i=1) ∧ x ∈ Point(face_lattice(J))
BY
(RepeatFor (DVar `f') THEN (InstHyp [⌜(i=1)⌝;⌜x⌝5⋅ THENA Auto) THEN -1 THEN Symmetry) }

1
1. fset(ℕ)
2. fset(ℕ)
3. J ⊆ I
4. Point(face_lattice(I)) ⟶ Point(face_lattice(J))
5. ∀[a,b:Point(face_lattice(I))].
     ((f a ∧ (f a ∧ b) ∈ Point(face_lattice(J))) ∧ (f a ∨ (f a ∨ b) ∈ Point(face_lattice(J))))
6. ((f 0) 0 ∈ Point(face_lattice(J))) ∧ ((f 1) 1 ∈ Point(face_lattice(J)))
7. ∀i:names(J). (((f (i=0)) (i=0) ∈ Point(face_lattice(J))) ∧ ((f (i=1)) (i=1) ∈ Point(face_lattice(J))))
8. Point(face_lattice(J))
9. (f x) x ∈ Point(face_lattice(J))
10. names(J)
11. (f (i=0) ∧ x) (i=0) ∧ x ∈ Point(face_lattice(J))
12. (i=1) ∧ (f (i=1) ∧ x) ∈ Point(face_lattice(J))
13. (i=1) ∨ (f (i=1) ∨ x) ∈ Point(face_lattice(J))
⊢ (i=1) ∧ (f (i=1) ∧ x) ∈ Point(face_lattice(J))


Latex:


Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  J  \msubseteq{}  I
4.  f  :  Hom(face\_lattice(I);face\_lattice(J))
5.  \mforall{}i:names(J).  (((f  (i=0))  =  (i=0))  \mwedge{}  ((f  (i=1))  =  (i=1)))
6.  x  :  Point(face\_lattice(J))
7.  (f  x)  =  x
8.  i  :  names(J)
9.  (f  (i=0)  \mwedge{}  x)  =  (i=0)  \mwedge{}  x
\mvdash{}  (f  (i=1)  \mwedge{}  x)  =  (i=1)  \mwedge{}  x


By


Latex:
(RepeatFor  2  (DVar  `f')  THEN  (InstHyp  [\mkleeneopen{}(i=1)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Symmetry)




Home Index