Step
*
1
of Lemma
lattice-extend-dlwc-inc
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. x : T
9. ↑fset-null({c ∈ Cs[x] | deq-f-subset(eq) c {x}})
⊢ \/(λxs./\(f"(xs))"({{x}})) = (f x) ∈ Point(L)
BY
{ (RepeatFor 2 (((RWO "fset-image-singleton" 0 THENA Auto) THEN Reduce 0))
THEN (RWO "lattice-fset-join-singleton" 0 THENA Auto)
THEN (RWO "lattice-fset-meet-singleton" 0 THENA Auto)) }
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. x : T
9. \muparrow{}fset-null(\{c \mmember{} Cs[x] | deq-f-subset(eq) c \{x\}\})
\mvdash{} \mbackslash{}/(\mlambda{}xs./\mbackslash{}(f"(xs))"(\{\{x\}\})) = (f x)
By
Latex:
(RepeatFor 2 (((RWO "fset-image-singleton" 0 THENA Auto) THEN Reduce 0))
THEN (RWO "lattice-fset-join-singleton" 0 THENA Auto)
THEN (RWO "lattice-fset-meet-singleton" 0 THENA Auto))
Home
Index