Step
*
1
of Lemma
empty-context-subset-lemma6
.....assertion.....
1. Gamma : CubicalSet{j}
2. x : Top × Top
3. y : Top × Top
⊢ ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I))
BY
{ (All Thin
THEN RepeatFor 2 ((D 0 THENA Auto))
THEN RepUR ``context-subset`` -1
THEN D -1
THEN RepUR ``face-0 cubical-term-at`` -1
THEN Assert ⌜¬(0 = 1 ∈ Point(face_lattice(I)))⌝⋅
THEN Auto) }
Latex:
Latex:
.....assertion.....
1. Gamma : CubicalSet\{j\}
2. x : Top \mtimes{} Top
3. y : Top \mtimes{} Top
\mvdash{} \mforall{}I:fset(\mBbbN{}). (\mneg{}Gamma, 0(\mBbbF{})(I))
By
Latex:
(All Thin
THEN RepeatFor 2 ((D 0 THENA Auto))
THEN RepUR ``context-subset`` -1
THEN D -1
THEN RepUR ``face-0 cubical-term-at`` -1
THEN Assert \mkleeneopen{}\mneg{}(0 = 1)\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index