---

Step * of Lemma face_lattice-hom-fixes-sublattice

∀[I,J:fset(ℕ)].
  ∀[f:Hom(face_lattice(J);face_lattice(I))]. ∀[x:Point(face_lattice(J))].
    (f x) = x ∈ Point(face_lattice(I)) 
    supposing ∀i:names(J)
                (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I)))) 
  supposing J ⊆ I
BY
{ (Intros THEN MoveToConcl (-2) THEN BLemma `face_lattice-induction` THEN Auto) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(J);face_lattice(I))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
⊢ (f 0) = 0 ∈ Point(face_lattice(I))

2
1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(J);face_lattice(I))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
⊢ (f 1) = 1 ∈ Point(face_lattice(I))

3
1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(J);face_lattice(I))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
6. x : Point(face_lattice(J))
7. y : Point(face_lattice(J))
8. (f x) = x ∈ Point(face_lattice(I))
9. (f y) = y ∈ Point(face_lattice(I))
⊢ (f x ∨ y) = x ∨ y ∈ Point(face_lattice(I))

4
1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(J);face_lattice(I))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
6. x : Point(face_lattice(J))
7. (f x) = x ∈ Point(face_lattice(I))
8. i : names(J)
⊢ (f (i=0) ∧ x) = (i=0) ∧ x ∈ Point(face_lattice(I))

5
1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(J);face_lattice(I))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
6. x : Point(face_lattice(J))
7. (f x) = x ∈ Point(face_lattice(I))
8. i : names(J)
9. (f (i=0) ∧ x) = (i=0) ∧ x ∈ Point(face_lattice(I))
⊢ (f (i=1) ∧ x) = (i=1) ∧ x ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].
    \mforall{}[f:Hom(face\_lattice(J);face\_lattice(I))].  \mforall{}[x:Point(face\_lattice(J))].
        (f  x)  =  x  supposing  \mforall{}i:names(J).  (((f  (i=0))  =  (i=0))  \mwedge{}  ((f  (i=1))  =  (i=1))) 
    supposing  J  \msubseteq{}  I


By

---

Latex:
(Intros  THEN  MoveToConcl  (-2)  THEN  BLemma  `face\_lattice-induction`  THEN  Auto)

---

Home Index