Step
*
1
1
1
1
of Lemma
oal_neg_non_id_vals
1. a : LOSet
2. b : AbDGrp
3. ps : (|a| × |b|) List
4. ¬↑(e ∈b map(λx.(snd(x));ps))
⊢ ¬↑(e ∈b map(λx.(~ (snd(x)));ps))
BY
{ (D 0 THENM D 4) THENA Auto }
1
1. a : LOSet
2. b : AbDGrp
3. ps : (|a| × |b|) List
4. ↑(e ∈b map(λx.(~ (snd(x)));ps))
⊢ ↑(e ∈b map(λx.(snd(x));ps))
Latex:
Latex:
1.  a  :  LOSet
2.  b  :  AbDGrp
3.  ps  :  (|a|  \mtimes{}  |b|)  List
4.  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps))
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(\msim{}  (snd(x)));ps))
By
Latex:
(D  0  THENM  D  4)  THENA  Auto
Home
Index