Step
*
1
of Lemma
irr-face-morph-satisfies
1. I : fset(ℕ)
2. as : fset(names(I))
3. bs : fset(names(I))
4. ↑fset-disjoint(NamesDeq;as;bs)
5. ∀a:names(I). (a ∈ as
⇒ ((irr-face-morph(I;as;bs) a) = 0 ∈ Point(dM(I))))
6. b : names(I)
7. b ∈ bs
8. b ∈ as
⊢ 0 = 1 ∈ Point(dM(I))
BY
{ ((RWO "assert-fset-disjoint" 4 THENA Auto) THEN (InstHyp [⌜b⌝] 4⋅ THENA Auto) THEN D -1 THEN Auto) }
Latex:
Latex:
1. I : fset(\mBbbN{})
2. as : fset(names(I))
3. bs : fset(names(I))
4. \muparrow{}fset-disjoint(NamesDeq;as;bs)
5. \mforall{}a:names(I). (a \mmember{} as {}\mRightarrow{} ((irr-face-morph(I;as;bs) a) = 0))
6. b : names(I)
7. b \mmember{} bs
8. b \mmember{} as
\mvdash{} 0 = 1
By
Latex:
((RWO "assert-fset-disjoint" 4 THENA Auto) THEN (InstHyp [\mkleeneopen{}b\mkleeneclose{}] 4\mcdot{} THENA Auto) THEN D -1 THEN Auto)
Home
Index