### Nuprl Lemma : bounded-lattice-hom-equal

`∀[l1,l2:BoundedLatticeStructure]. ∀[f,g:Hom(l1;l2)].`
`  f = g ∈ Hom(l1;l2) supposing ∀x:Point(l1). ((f x) = (g x) ∈ Point(l2))`

Proof

Definitions occuring in Statement :  bounded-lattice-hom: `Hom(l1;l2)` bounded-lattice-structure: `BoundedLatticeStructure` lattice-point: `Point(l)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bounded-lattice-hom: `Hom(l1;l2)` and: `P ∧ Q` lattice-hom: `Hom(l1;l2)` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  equal_wf squash_wf true_wf lattice-point_wf bounded-lattice-structure-subtype iff_weakening_equal uall_wf lattice-meet_wf lattice-join_wf lattice-0_wf lattice-1_wf all_wf bounded-lattice-hom_wf bounded-lattice-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality productElimination functionExtensionality applyEquality lambdaEquality imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality sqequalRule dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination because_Cache productEquality isect_memberEquality axiomEquality

Latex:
\mforall{}[l1,l2:BoundedLatticeStructure].  \mforall{}[f,g:Hom(l1;l2)].    f  =  g  supposing  \mforall{}x:Point(l1).  ((f  x)  =  (g  x))

Date html generated: 2017_10_05-AM-00_30_38
Last ObjectModification: 2017_07_28-AM-09_12_39

Theory : lattices

Home Index