Step
*
1
2
of Lemma
cal-filter_wf
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. s : fset(fset(T))
5. (↑fset-antichain(eq;s)) ∧ fset-all(s;a.P a)
6. Q : {x:fset(T)| ↑P[x]} ⟶ 𝔹
7. {x ∈ s | Q[x]} ∈ fset({x:fset(T)| ↑P[x]} )
⊢ cal-filter(s;x.Q[x]) ∈ {ac:fset({x:fset(T)| ↑P[x]} )| ↑fset-antichain(eq;ac)}
BY
{ (Unfold `cal-filter` 0 THEN MemTypeCD THEN Auto) }
1
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. {x ∈ s | Q[x]} ∈ fset({x:fset(T)| ↑P[x]} )
⊢ ↑fset-antichain(eq;{x ∈ s | Q[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)) \mwedge{} fset-all(s;a.P a)
6. Q : \{x:fset(T)| \muparrow{}P[x]\} {}\mrightarrow{} \mBbbB{}
7. \{x \mmember{} s | Q[x]\} \mmember{} fset(\{x:fset(T)| \muparrow{}P[x]\} )
\mvdash{} cal-filter(s;x.Q[x]) \mmember{} \{ac:fset(\{x:fset(T)| \muparrow{}P[x]\} )| \muparrow{}fset-antichain(eq;ac)\}
By
Latex:
(Unfold `cal-filter` 0 THEN MemTypeCD THEN Auto)
Home
Index