### Nuprl Lemma : fdl-hom-agrees

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

Proof

Definitions occuring in Statement :  fdl-hom: `fdl-hom(L;f)` free-dl-generator: `free-dl-generator(x)` bdd-distributive-lattice: `BoundedDistributiveLattice` lattice-point: `Point(l)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` free-dl-generator: `free-dl-generator(x)` fdl-hom: `fdl-hom(L;f)` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` bdd-distributive-lattice: `BoundedDistributiveLattice` so_lambda: `λ2x.t[x]` and: `P ∧ Q` so_apply: `x[s]` uimplies: `b supposing a` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  list_accum_cons_lemma list_accum_nil_lemma equal_wf squash_wf true_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 lattice-0_wf lattice-1-meet bdd-distributive-lattice-subtype-bdd-lattice iff_weakening_equal lattice-join-0 bdd-distributive-lattice_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis applyEquality lambdaEquality imageElimination isectElimination hypothesisEquality equalityTransitivity equalitySymmetry because_Cache instantiate productEquality independent_isectElimination setElimination rename functionExtensionality cumulativity natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination axiomEquality functionEquality

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

Date html generated: 2017_10_05-AM-00_32_58
Last ObjectModification: 2017_07_28-AM-09_13_34

Theory : lattices

Home Index