Step
*
1
1
of Lemma
cal-filter-decomp
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. s : fset(fset(T))
5. ↑fset-antichain(eq;s)
6. fset-all(s;a.P a)
7. Q : {x:fset(T)| ↑P[x]} ⟶ 𝔹
8. cal-filter(s;x.Q[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)}
9. cal-filter(s;x.¬bQ[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)}
10. least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2)\000C;
cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x]);lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x])))
11. Order({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
12. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);s)
13. x : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])}
14. fset-ac-le(eq;cal-filter(s;x.Q[x]);x)
15. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);x)
⊢ fset-ac-le(eq;s;x)
BY
{ Assert ⌜s ∈ fset({x:fset(T)| ↑P[x]} )⌝⋅ }
1
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. s : fset(fset(T))
5. ↑fset-antichain(eq;s)
6. fset-all(s;a.P a)
7. Q : {x:fset(T)| ↑P[x]} ⟶ 𝔹
8. cal-filter(s;x.Q[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)}
9. cal-filter(s;x.¬bQ[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)}
10. least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2)\000C;
cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x]);lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x])))
11. Order({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
12. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);s)
13. x : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])}
14. fset-ac-le(eq;cal-filter(s;x.Q[x]);x)
15. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);x)
⊢ s ∈ fset({x:fset(T)| ↑P[x]} )
2
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. s : fset(fset(T))
5. ↑fset-antichain(eq;s)
6. fset-all(s;a.P a)
7. Q : {x:fset(T)| ↑P[x]} ⟶ 𝔹
8. cal-filter(s;x.Q[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)}
9. cal-filter(s;x.¬bQ[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)}
10. least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2)\000C;
cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x]);lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x])))
11. Order({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
12. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);s)
13. x : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])}
14. fset-ac-le(eq;cal-filter(s;x.Q[x]);x)
15. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);x)
16. s ∈ fset({x:fset(T)| ↑P[x]} )
⊢ fset-ac-le(eq;s;x)
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) {}\mrightarrow{} \mBbbB{}
4. s : fset(fset(T))
5. \muparrow{}fset-antichain(eq;s)
6. fset-all(s;a.P a)
7. Q : \{x:fset(T)| \muparrow{}P[x]\} {}\mrightarrow{} \mBbbB{}
8. cal-filter(s;x.Q[x]) \mmember{} \{ac:fset(fset(T))| (\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;a.P a)\}
9. cal-filter(s;x.\mneg{}\msubb{}Q[x]) \mmember{} \{ac:fset(fset(T))| (\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;a.P a)\}
10. least-upper-bound(\{ac:fset(fset(T))| (\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;a.P[a])\} ;
ac1,ac2.fset-ac-le(eq;ac1;ac2);
cal-filter(s;x.Q[x]);cal-filter(s;x.\mneg{}\msubb{}Q[x]);lub(P;cal-filter(s;x.Q[x]);...))
11. Order(\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
12. fset-ac-le(eq;cal-filter(s;x.\mneg{}\msubb{}Q[x]);s)
13. x : \{ac:fset(fset(T))| (\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;a.P[a])\}
14. fset-ac-le(eq;cal-filter(s;x.Q[x]);x)
15. fset-ac-le(eq;cal-filter(s;x.\mneg{}\msubb{}Q[x]);x)
\mvdash{} fset-ac-le(eq;s;x)
By
Latex:
Assert \mkleeneopen{}s \mmember{} fset(\{x:fset(T)| \muparrow{}P[x]\} )\mkleeneclose{}\mcdot{}
Home
Index