---

Step * of Lemma map-to-context-subset-disjoint

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[H:j⊢].
  ∀[sigma:H j⟶ Gamma, (phi ∧ psi)]. ∀[I:fset(ℕ)].  (¬H(I)) supposing Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -3
   THEN Thin (-3)
   THEN RepUR ``cube-cat op-cat type-cat context-subset`` -3
   THEN Fold `I_cube` (-3)
   THEN Fold `implies` (-3)
   THEN Fold `all` (-3)
   THEN InstHyp [⌜I⌝] (-3)⋅
   THEN Auto) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. H : CubicalSet{j}
5. Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽))
6. sigma : ∀A:fset(ℕ). (H(A) ⇒ {rho:Gamma(A)| (phi ∧ psi)(rho) = 1 ∈ Point(face_lattice(A))} )
7. I : fset(ℕ)
8. H(I)
9. {rho:Gamma(I)| (phi ∧ psi)(rho) = 1 ∈ Point(face_lattice(I))} 
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[H:j\mvdash{}].
    \mforall{}[sigma:H  j{}\mrightarrow{}  Gamma,  (phi  \mwedge{}  psi)].  \mforall{}[I:fset(\mBbbN{})].    (\mneg{}H(I))  supposing  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -3
  THEN  Thin  (-3)
  THEN  RepUR  ``cube-cat  op-cat  type-cat  context-subset``  -3
  THEN  Fold  `I\_cube`  (-3)
  THEN  Fold  `implies`  (-3)
  THEN  Fold  `all`  (-3)
  THEN  InstHyp  [\mkleeneopen{}I\mkleeneclose{}]  (-3)\mcdot{}
  THEN  Auto)

---

Home Index