Step
*
2
1
1
1
of Lemma
lattice-extend-wc-meet
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T ⟶ Point(L)
7. ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
8. a : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))}
9. b : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))}
10. ∀[s:fset(fset(T))]. (λls./\(ls)"(λxs.f"(xs)"(s)) = λx./\(f"(x))"(s) ∈ fset(Point(L)))
⊢ \/(λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);λxs.f"(xs)"(a);as.λbs.as ⋃ bs"(λxs.f"(xs)"(b)))))
≤ \/(λls./\(ls)"(λxs.f"(xs)"
(f-union(deq-fset(eq);deq-fset(eq);a;as.λbs.as ⋃ bs"(b) s.t. λs.fset-contains-none(eq;s;x.Cs[x])))))
BY
{ (Using [`eq',⌜eqL⌝] (BLemma lattice-fset-join_functionality_wrt_subset2)⋅
THEN Auto
THEN (D 0 THENA Auto)
THEN RenameVar `x' (-1)
THEN (D 0 THENA Auto)) }
1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T ⟶ Point(L)
7. ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
8. a : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))}
9. b : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))}
10. ∀[s:fset(fset(T))]. (λls./\(ls)"(λxs.f"(xs)"(s)) = λx./\(f"(x))"(s) ∈ fset(Point(L)))
11. x : Point(L)
12. x ∈ λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);λxs.f"(xs)"(a);as.λbs.as ⋃ bs"(λxs.f"(xs)"(b))))
⊢ x ∈ {0} ⋃ λls./\(ls)"
(λxs.f"(xs)"
(f-union(deq-fset(eq);deq-fset(eq);a;as.λbs.as ⋃ bs"(b) s.t. λs.fset-contains-none(eq;s;x.Cs[x]))))
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. Cs : T {}\mrightarrow{} fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T {}\mrightarrow{} Point(L)
7. \mforall{}x:T. \mforall{}c:fset(T). (c \mmember{} Cs[x] {}\mRightarrow{} (/\mbackslash{}(f"(c)) = 0))
8. a : \{ac:fset(fset(T))|
(\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))\}
9. b : \{ac:fset(fset(T))|
(\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))\}
10. \mforall{}[s:fset(fset(T))]. (\mlambda{}ls./\mbackslash{}(ls)"(\mlambda{}xs.f"(xs)"(s)) = \mlambda{}x./\mbackslash{}(f"(x))"(s))
\mvdash{} \mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);\mlambda{}xs.f"(xs)"(a);as.\mlambda{}bs.as \mcup{} bs"
(\mlambda{}xs.f"(xs)"(b)))))
\mleq{} \mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"
(\mlambda{}xs.f"(xs)"
(f-union(deq-fset(eq);deq-fset(eq);a;as.\mlambda{}bs.as \mcup{} bs"(b) s.t. \mlambda{}s....))))
By
Latex:
(Using [`eq',\mkleeneopen{}eqL\mkleeneclose{}] (BLemma lattice-fset-join\_functionality\_wrt\_subset2)\mcdot{}
THEN Auto
THEN (D 0 THENA Auto)
THEN RenameVar `x' (-1)
THEN (D 0 THENA Auto))
Home
Index