---

Step * of Lemma constrained-antichain-lattice_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹].
  constrained-antichain-lattice(T;eq;P) ∈ BoundedDistributiveLattice 
  supposing (∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))) ∧ (↑(P {}))
BY
{ (Auto
   THEN Unfold `constrained-antichain-lattice` 0
   THEN Using [`R',⌜λ2ac1 ac2.fset-ac-le(eq;ac1;ac2)⌝] (BLemma `mk-bounded-distributive-lattice-from-order`)⋅
   THEN RepUR ``so_apply`` 0
   THEN Auto) }

1
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
5. ↑(P {})
⊢ {{}} ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 

2
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
5. ↑(P {})
6. Order({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y))
7. a : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 
8. b : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 
⊢ least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y);
                    a;b;lub(P;a;b))

3
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
5. ↑(P {})
6. Order({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y))
7. ∀[a,b:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ].
     least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y);
                       a;b;lub(P;a;b))
8. a : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 
9. b : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 
⊢ greatest-lower-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y);a;b;glb\000C(P;a;b))

4
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
5. ↑(P {})
6. Order({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y))
7. ∀[a,b:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ].
     least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y);
                       a;b;lub(P;a;b))
8. ∀[a,b:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ].
     greatest-lower-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;x,y.fset-ac-le(eq;x;y);a;b;\000Cglb(P;a;b))
9. ∀[a:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ]. fset-ac-le(eq;a;{{}})
10. a : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 
⊢ fset-ac-le(eq;{};a)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].
    constrained-antichain-lattice(T;eq;P)  \mmember{}  BoundedDistributiveLattice 
    supposing  (\mforall{}x,y:fset(T).    (y  \msubseteq{}  x  {}\mRightarrow{}  (\muparrow{}(P  x))  {}\mRightarrow{}  (\muparrow{}(P  y))))  \mwedge{}  (\muparrow{}(P  \{\}))


By

---

Latex:
(Auto
  THEN  Unfold  `constrained-antichain-lattice`  0
  THEN  Using  [`R',\mkleeneopen{}\mlambda{}\msubtwo{}ac1  ac2.fset-ac-le(eq;ac1;ac2)\mkleeneclose{}
  ]  (BLemma  `mk-bounded-distributive-lattice-from-order`)\mcdot{}
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto)

---

Home Index