Nuprl Lemma : lattice-meet-join-images-distrib

L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀as,bs:fset(fset(Point(L))).
  (\/(λls./\(ls)"(as)) ∧ \/(λls./\(ls)"(bs))
  \/(λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.λbs.as ⋃ bs"(bs))))
  ∈ Point(L))


Proof




Definitions occuring in Statement :  lattice-fset-join: \/(s) lattice-fset-meet: /\(s) bdd-distributive-lattice: BoundedDistributiveLattice lattice-meet: a ∧ b lattice-point: Point(l) fset-image: f"(s) deq-fset: deq-fset(eq) f-union: f-union(domeq;rngeq;s;x.g[x]) fset-union: x ⋃ y fset: fset(T) deq: EqDecider(T) all: x:A. B[x] lambda: λx.A[x] equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T squash: T prop: subtype_rel: A ⊆B implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] true: True uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q bdd-distributive-lattice: BoundedDistributiveLattice uiff: uiff(P;Q) sq_stable: SqStable(P) exists: x:A. B[x] cand: c∧ B fset-union: x ⋃ y l-union: as ⋃ bs reduce: reduce(f;k;as) list_ind: list_ind lattice-fset-meet: /\(s)
Lemmas referenced :  lattice-meet-fset-join-distrib equal_wf squash_wf true_wf fset-image_wf deq-fset_wf lattice-fset-meet_wf bdd-distributive-lattice-subtype-bdd-lattice decidable-equal-deq lattice-fset-join_wf f-union_wf fset-union_wf iff_weakening_equal fset_wf lattice-point_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf uall_wf lattice-meet_wf lattice-join_wf deq_wf bdd-distributive-lattice_wf fset-extensionality fset-member_witness fset-member_wf sq_stable__fset-member member-fset-image-iff member-f-union lattice-fset-meet-union
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality lambdaEquality imageElimination equalityTransitivity hypothesis equalitySymmetry universeEquality because_Cache sqequalRule independent_functionElimination dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination instantiate productEquality cumulativity isect_memberFormation independent_pairFormation independent_pairEquality isect_memberEquality hyp_replacement applyLambdaEquality dependent_pairFormation

Latex:
\mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).  \mforall{}as,bs:fset(fset(Point(L))).
    (\mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(as))  \mwedge{}  \mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(bs))
    =  \mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.\mlambda{}bs.as  \mcup{}  bs"(bs)))))



Date html generated: 2020_05_20-AM-08_46_00
Last ObjectModification: 2017_07_28-AM-09_14_41

Theory : lattices


Home Index