---

Step * of Lemma cal-filter_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:Point(constrained-antichain-lattice(T;eq;P))]. ∀[Q:{x:fset(T)| 
                                                                                                          ↑P[x]}  ⟶ 𝔹].
  (cal-filter(s;x.Q[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)))
BY
{ ((RepeatFor 3 ((Intro THENA Auto)) THEN (RWO "cal-point" 0 THENA Auto))
   THEN Auto
   THEN DVar `s'
   THEN SubsumeC ⌜{ac:fset({x:fset(T)| ↑P[x]} )| ↑fset-antichain(eq;ac)} ⌝⋅) }

1
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]}  ⟶ 𝔹
⊢ cal-filter(s;x.Q[x]) ∈ {ac:fset({x:fset(T)| ↑P[x]} )| ↑fset-antichain(eq;ac)} 

2
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. cal-filter(s;x.Q[x]) = cal-filter(s;x.Q[x]) ∈ {ac:fset({x:fset(T)| ↑P[x]} )| ↑fset-antichain(eq;ac)} 
⊢ {ac:fset({x:fset(T)| ↑P[x]} )| ↑fset-antichain(eq;ac)}  ⊆r {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a\000C.P a)} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:Point(constrained-antichain-lattice(T;eq;P))].
\mforall{}[Q:\{x:fset(T)|  \muparrow{}P[x]\}    {}\mrightarrow{}  \mBbbB{}].
    (cal-filter(s;x.Q[x])  \mmember{}  Point(constrained-antichain-lattice(T;eq;P)))


By

---

Latex:
((RepeatFor  3  ((Intro  THENA  Auto))  THEN  (RWO  "cal-point"  0  THENA  Auto))
  THEN  Auto
  THEN  DVar  `s'
  THEN  SubsumeC  \mkleeneopen{}\{ac:fset(\{x:fset(T)|  \muparrow{}P[x]\}  )|  \muparrow{}fset-antichain(eq;ac)\}  \mkleeneclose{}\mcdot{})

---

Home Index