Nuprl Lemma : free-dl-generators

`∀[X:Type]`
`  ∀L:BoundedDistributiveLattice`
`    ∀[f,g:Hom(free-dl(X);L)].`
`      f = g ∈ Hom(free-dl(X);L) supposing ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))`

Proof

Definitions occuring in Statement :  free-dl-generator: `free-dl-generator(x)` free-dl: `free-dl(X)` bdd-distributive-lattice: `BoundedDistributiveLattice` bounded-lattice-hom: `Hom(l1;l2)` lattice-point: `Point(l)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` lattice-point: `Point(l)` record-select: `r.x` free-dl: `free-dl(X)` mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: `mk-bounded-lattice(T;m;j;z;o)` record-update: `r[x := v]` ifthenelse: `if b then t else f fi ` eq_atom: `x =a y` bfalse: `ff` btrue: `tt` free-dl-type: `free-dl-type(X)` quotient: `x,y:A//B[x; y]` member: `t ∈ T` subtype_rel: `A ⊆r B` bdd-distributive-lattice: `BoundedDistributiveLattice` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` uimplies: `b supposing a` all: `∀x:A. B[x]` bounded-lattice-hom: `Hom(l1;l2)` lattice-hom: `Hom(l1;l2)` guard: `{T}` implies: `P `` Q` cand: `A c∧ B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` squash: `↓T` true: `True` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` append: `as @ bs` list_ind: list_ind lattice-join: `a ∨ b` free-dl-join: `free-dl-join(as;bs)` listp: `A List+` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cons: `[a / b]` lattice-meet: `a ∧ b` free-dl-meet: `free-dl-meet(as;bs)` list_accum: list_accum nil: `[]` it: `⋅` map: `map(f;as)` free-dl-generator: `free-dl-generator(x)` lattice-1: `1` lattice-0: `0`
Lemmas referenced :  lattice-point_wf free-dl_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf uall_wf equal_wf lattice-meet_wf lattice-join_wf lattice-0_wf lattice-1_wf all_wf free-dl-generator_wf subtype_rel_weakening ext-eq_weakening bounded-lattice-hom_wf bdd-distributive-lattice_wf dlattice-eq-equiv list_wf dlattice-eq_wf quotient-member-eq subtype_quotient equal-wf-base squash_wf true_wf accum_induction cons_wf_listp nil_wf less_than_wf length_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut sqequalRule hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality applyEquality instantiate lambdaEquality productEquality universeEquality because_Cache independent_isectElimination lambdaFormation setElimination rename dependent_set_memberEquality productElimination functionExtensionality equalityTransitivity equalitySymmetry isect_memberEquality axiomEquality promote_hyp independent_pairFormation dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality pointwiseFunctionality pertypeElimination imageElimination natural_numberEquality imageMemberEquality baseClosed equalityUniverse levelHypothesis

Latex:
\mforall{}[X:Type]
\mforall{}L:BoundedDistributiveLattice
\mforall{}[f,g:Hom(free-dl(X);L)].
f  =  g  supposing  \mforall{}x:X.  ((f  free-dl-generator(x))  =  (g  free-dl-generator(x)))

Date html generated: 2017_10_05-AM-00_32_31
Last ObjectModification: 2017_07_28-AM-09_13_30

Theory : lattices

Home Index