Step
*
of Lemma
lattice-extend-meet
No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
∀[a,b:Point(free-dist-lattice(T; eq))].
lattice-extend(L;eq;eqL;f;a) ∧ lattice-extend(L;eq;eqL;f;b) ≤ lattice-extend(L;eq;eqL;f;a ∧ b)
BY
{ (Auto
THEN (RWO "free-dl-meet" 0 THENA Auto)
THEN Unfold `lattice-extend` 0
THEN Fold `lattice-extend\'` 0
THEN All (RWO "free-dl-point")
THEN Auto
THEN (Using [`b',⌜lattice-extend'(L;eq;eqL;f;f-union(deq-fset(eq);deq-fset(eq);a;as.λbs.as ⋃ bs"(b)))⌝
] (BLemma `lattice-le_transitivity`)⋅
THENA Auto
)) }
1
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
6. a : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
7. b : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
⊢ lattice-extend'(L;eq;eqL;f;f-union(deq-fset(eq);deq-fset(eq);a;as.λbs.as ⋃ bs"(b)))
≤ lattice-extend'(L;eq;eqL;f;fset-ac-glb(eq;a;b))
2
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
6. a : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
7. b : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
⊢ lattice-extend'(L;eq;eqL;f;a) ∧ lattice-extend'(L;eq;eqL;f;b)
≤ lattice-extend'(L;eq;eqL;f;f-union(deq-fset(eq);deq-fset(eq);a;as.λbs.as ⋃ bs"(b)))
Latex:
Latex:
No Annotations
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[L:BoundedDistributiveLattice]. \mforall{}[eqL:EqDecider(Point(L))].
\mforall{}[f:T {}\mrightarrow{} Point(L)]. \mforall{}[a,b:Point(free-dist-lattice(T; eq))].
lattice-extend(L;eq;eqL;f;a) \mwedge{} lattice-extend(L;eq;eqL;f;b) \mleq{} lattice-extend(L;eq;eqL;f;a \mwedge{} b)
By
Latex:
(Auto
THEN (RWO "free-dl-meet" 0 THENA Auto)
THEN Unfold `lattice-extend` 0
THEN Fold `lattice-extend\mbackslash{}'` 0
THEN All (RWO "free-dl-point")
THEN Auto
THEN (Using [`b',\mkleeneopen{}lattice-extend'(L;eq;eqL;f;f-union(deq-fset(eq);deq-fset(eq);a;as.\mlambda{}bs.as \mcup{} bs"
(b)))\mkleeneclose{}
] (BLemma `lattice-le\_transitivity`)\mcdot{}
THENA Auto
))
Home
Index