Step
*
1
1
1
1
of Lemma
poset_functor_extend-face-map1
.....equality.....
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
12. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
13. I ∈ nameset(I) List
14. CnameDeq ∈ EqDecider(nameset(I))
15. ((y:=a) o c1) ∈ name-morph(I;[])
16. ((y:=a) o c2) ∈ name-morph(I;[])
⊢ filter(λx.((((y:=a) o c1) x =z 0) ∧b (((y:=a) o c2) x =z 1));I) ~ filter(λx.((((y:=a) o c1) x =z 0)
∧b (((y:=a) o c2) x =z 1));I-[y])
BY
{ ((RWO "filter-list-diff" 0 THENA Auto) THEN Reduce 0 THEN SplitOnConclITE THEN Auto) }
1
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
12. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
13. I ∈ nameset(I) List
14. CnameDeq ∈ EqDecider(nameset(I))
15. ((y:=a) o c1) ∈ name-morph(I;[])
16. ((y:=a) o c2) ∈ name-morph(I;[])
17. (((y:=a) o c1) y) = 0 ∈ ℤ
18. (((y:=a) o c2) y) = 1 ∈ ℤ
⊢ filter(λx.((((y:=a) o c1) x =z 0) ∧b (((y:=a) o c2) x =z 1));I)
= filter(λx.((((y:=a) o c1) x =z 0) ∧b (((y:=a) o c2) x =z 1));I)-[y]
∈ (nameset(I) List)
Latex:
Latex:
.....equality.....
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) {}\mrightarrow{} cat-ob(C)
4. E : i:nameset(I) {}\mrightarrow{} c:\{c:name-morph(I;[])| (c i) = 0\} {}\mrightarrow{} (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : \mBbbN{}2
7. n : \mBbbN{}
8. \mforall{}n:\mBbbN{}n
\mforall{}[c1,c2:name-morph(I;[])].
((||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n)
{}\mRightarrow{} poset\_functor\_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset\_functor\_extend(C;I-[y];L o (\mlambda{}f.((y:=a) o f));\mlambda{}z,f. (E z ((y:=a) o f));c1;c2)
supposing \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n
12. \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x))
13. I \mmember{} nameset(I) List
14. CnameDeq \mmember{} EqDecider(nameset(I))
15. ((y:=a) o c1) \mmember{} name-morph(I;[])
16. ((y:=a) o c2) \mmember{} name-morph(I;[])
\mvdash{} filter(\mlambda{}x.((((y:=a) o c1) x =\msubz{} 0) \mwedge{}\msubb{} (((y:=a) o c2) x =\msubz{} 1));I)
\msim{} filter(\mlambda{}x.((((y:=a) o c1) x =\msubz{} 0) \mwedge{}\msubb{} (((y:=a) o c2) x =\msubz{} 1));I-[y])
By
Latex:
((RWO "filter-list-diff" 0 THENA Auto) THEN Reduce 0 THEN SplitOnConclITE THEN Auto)
Home
Index