Step
*
of Lemma
s-comp-0-e'
∀[I:fset(ℕ)]. ∀[i:ℕ]. ∀[J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[j:{j:ℕ| ¬j ∈ I} ]. ∀[k:{j:ℕ| ¬j ∈ J} ].
(s ⋅ (i0) ⋅ f,j=k = (i0) ⋅ f ⋅ s ∈ J+k ⟶ I+i)
BY
{ (Auto
THEN DSetVars
THEN (RWW "nh-comp-assoc nc-0-s-commute<" 0 THENA Auto)
THEN RWW "nh-comp-assoc< nc-e\'-lemma3" 0
THEN Auto) }
Latex:
Latex:
\mforall{}[I:fset(\mBbbN{})]. \mforall{}[i:\mBbbN{}]. \mforall{}[J:fset(\mBbbN{})]. \mforall{}[f:J {}\mrightarrow{} I]. \mforall{}[j:\{j:\mBbbN{}| \mneg{}j \mmember{} I\} ]. \mforall{}[k:\{j:\mBbbN{}| \mneg{}j \mmember{} J\} ].
(s \mcdot{} (i0) \mcdot{} f,j=k = (i0) \mcdot{} f \mcdot{} s)
By
Latex:
(Auto
THEN DSetVars
THEN (RWW "nh-comp-assoc nc-0-s-commute<" 0 THENA Auto)
THEN RWW "nh-comp-assoc< nc-e\mbackslash{}'-lemma3" 0
THEN Auto)
Home
Index