Nuprl Lemma : fdl-hom_wf

`∀[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)].  (fdl-hom(L;f) ∈ Hom(free-dl(X);L))`

Proof

Definitions occuring in Statement :  fdl-hom: `fdl-hom(L;f)` free-dl: `free-dl(X)` bdd-distributive-lattice: `BoundedDistributiveLattice` bounded-lattice-hom: `Hom(l1;l2)` lattice-point: `Point(l)` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` 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` fdl-hom: `fdl-hom(L;f)` list_accum: list_accum lattice-0: `0` 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` nil: `[]` it: `⋅` lattice-1: `1` cons: `[a / b]` lattice-join: `a ∨ b` all: `∀x:A. B[x]` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` free-dl-join: `free-dl-join(as;bs)` append: `as @ bs` list_ind: list_ind implies: `P `` Q` nat: `ℕ` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` or: `P ∨ Q` le: `A ≤ B` less_than': `less_than'(a;b)` colength: `colength(L)` guard: `{T}` sq_type: `SQType(T)` less_than: `a < b` squash: `↓T` decidable: `Dec(P)` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` free-dl-type: `free-dl-type(X)` cand: `A c∧ B` dlattice-eq: `dlattice-eq(X;as;bs)` quotient: `x,y:A//B[x; y]` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` dlattice-order: `as `` bs` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` lelt: `i ≤ j < k` select: `L[n]` lattice-le: `a ≤ b` l_contains: `A ⊆ B` nat_plus: `ℕ+` uiff: `uiff(P;Q)` istype: `istype(T)` order: `Order(T;x,y.R[x; y])` anti_sym: `AntiSym(T;x,y.R[x; y])` lattice-point: `Point(l)` bounded-lattice-hom: `Hom(l1;l2)` lattice-hom: `Hom(l1;l2)` sym: `Sym(T;x,y.E[x; y])` lattice-meet: `a ∧ b` free-dl-meet: `free-dl-meet(as;bs)` map: `map(f;as)` listp: `A List+` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  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 equal_wf lattice-meet_wf lattice-join_wf bdd-distributive-lattice_wf istype-universe lattice-0_wf lattice-join-0 bdd-distributive-lattice-subtype-bdd-lattice lattice-1_wf list_accum_nil_lemma istype-void list_wf list_accum_append subtype_rel_list top_wf fdl-hom_wf1 nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than list-cases product_subtype_list colength-cons-not-zero colength_wf_list istype-false istype-le subtract-1-ge-0 subtype_base_sq intformeq_wf int_formula_prop_eq_lemma set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int subtract_wf intformnot_wf itermSubtract_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_subtract_lemma int_term_value_add_lemma decidable__le le_wf list_accum_cons_lemma istype-nat unit_wf2 unit_subtype_base it_wf squash_wf true_wf subtype_rel_self iff_weakening_equal cons_wf list_accum_wf lattice_properties bdd-distributive-lattice-subtype-lattice dlattice-eq-equiv dlattice-eq_wf member_wf free-dl-type_wf last_induction all_wf dlattice-order_wf lattice-le_wf nil_wf append_wf lattice-0-le lattice-join-le l_all_append l_exists_wf l_member_wf l_contains_wf length_of_cons_lemma length_of_nil_lemma l_exists_iff lattice-le_transitivity null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse cons_member lattice-le_weakening le-lattice-1 l_all_cons add_nat_plus length_wf_nat nat_plus_properties decidable__lt add-is-int-iff false_wf length_wf lattice-meet-le lattice-le-meet lattice-le-order free-dl_wf quotient-member-eq subtype_quotient free-dl-meet_wf lattice-meet-0 cons_wf_listp less_than_wf distributive-lattice-distrib bdd-distributive-lattice-subtype-distributive-lattice free-dl-meet_wf_list list_ind_nil_lemma map_nil_lemma lattice-0-meet map_cons_lemma map_wf lattice-meet-1 lattice-1-meet
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionIsType universeIsType hypothesisEquality extract_by_obid isectElimination thin applyEquality instantiate lambdaEquality_alt productEquality cumulativity inhabitedIsType because_Cache independent_isectElimination isect_memberEquality_alt isectIsTypeImplies universeEquality independent_pairFormation setElimination rename productElimination dependent_functionElimination voidElimination lambdaFormation_alt equalityIsType1 independent_functionElimination intWeakElimination natural_numberEquality approximateComputation dependent_pairFormation_alt int_eqEquality functionIsTypeImplies unionElimination promote_hyp hypothesis_subsumption dependent_set_memberEquality_alt applyLambdaEquality imageElimination equalityIsType4 baseApply closedConclusion baseClosed intEquality imageMemberEquality functionExtensionality pointwiseFunctionality pertypeElimination productIsType functionEquality setIsType hyp_replacement addEquality independent_pairEquality isectIsType

Latex:
\mforall{}[X:Type].  \mforall{}[L:BoundedDistributiveLattice].  \mforall{}[f:X  {}\mrightarrow{}  Point(L)].    (fdl-hom(L;f)  \mmember{}  Hom(free-dl(X);L))

Date html generated: 2019_10_31-AM-07_20_49
Last ObjectModification: 2018_11_13-AM-10_25_36

Theory : lattices

Home Index