Nuprl Lemma : dM-homs-equal
∀[I:fset(ℕ)]. ∀[l:BoundedLattice].
  ∀eq:EqDecider(Point(l))
    ∀[h1,h2:Hom(dM(I);l)].
      h1 = h2 ∈ (Point(dM(I)) ⟶ Point(l)) 
      supposing ∀i:names(I). (((h1 <i>) = (h2 <i>) ∈ Point(l)) ∧ ((h1 <1-i>) = (h2 <1-i>) ∈ Point(l)))
Proof
Definitions occuring in Statement : 
dM_opp: <1-x>
, 
dM_inc: <x>
, 
dM: dM(I)
, 
names: names(I)
, 
bounded-lattice-hom: Hom(l1;l2)
, 
bdd-lattice: BoundedLattice
, 
lattice-point: Point(l)
, 
fset: fset(T)
, 
deq: EqDecider(T)
, 
nat: ℕ
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
all: ∀x:A. B[x]
, 
and: P ∧ Q
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
all: ∀x:A. B[x]
, 
uimplies: b supposing a
, 
subtype_rel: A ⊆r B
, 
DeMorgan-algebra: DeMorganAlgebra
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
guard: {T}
, 
prop: ℙ
, 
and: P ∧ Q
, 
bdd-lattice: BoundedLattice
, 
bounded-lattice-hom: Hom(l1;l2)
, 
lattice-hom: Hom(l1;l2)
, 
implies: P 
⇒ Q
, 
squash: ↓T
, 
true: True
, 
iff: P 
⇐⇒ Q
, 
rev_implies: P 
⇐ Q
, 
top: Top
, 
free-dl-inc: free-dl-inc(x)
, 
fset-singleton: {x}
, 
cons: [a / b]
, 
nil: []
, 
it: ⋅
, 
dM_inc: <x>
, 
dminc: <i>
, 
dM_opp: <1-x>
, 
dmopp: <1-i>
Lemmas referenced : 
dM-hom-basis, 
lattice-point_wf, 
dM_wf, 
subtype_rel_set, 
lattice-structure_wf, 
bounded-lattice-structure-subtype, 
DeMorgan-algebra-structure-subtype, 
subtype_rel_transitivity, 
all_wf, 
names_wf, 
equal_wf, 
bounded-lattice-structure_wf, 
lattice-axioms_wf, 
bounded-lattice-axioms_wf, 
dM_inc_wf, 
dM_opp_wf, 
bounded-lattice-hom_wf, 
DeMorgan-algebra-structure_wf, 
uall_wf, 
lattice-meet_wf, 
lattice-join_wf, 
DeMorgan-algebra-axioms_wf, 
deq_wf, 
bdd-lattice_wf, 
fset_wf, 
nat_wf, 
deq-implies, 
squash_wf, 
true_wf, 
iff_weakening_equal, 
lattice-fset-join_wf, 
decidable_wf, 
dM-point, 
fset-image_wf, 
deq-fset_wf, 
union-deq_wf, 
names-deq_wf, 
lattice-fset-meet_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
lambdaFormation, 
functionExtensionality, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
dependent_functionElimination, 
because_Cache, 
hypothesis, 
applyEquality, 
sqequalRule, 
instantiate, 
independent_isectElimination, 
lambdaEquality, 
productEquality, 
cumulativity, 
setElimination, 
rename, 
isect_memberEquality, 
axiomEquality, 
equalityTransitivity, 
equalitySymmetry, 
universeEquality, 
independent_functionElimination, 
imageElimination, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
productElimination, 
voidElimination, 
voidEquality, 
unionEquality, 
unionElimination
Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[l:BoundedLattice].
    \mforall{}eq:EqDecider(Point(l))
        \mforall{}[h1,h2:Hom(dM(I);l)].
            h1  =  h2  supposing  \mforall{}i:names(I).  (((h1  <i>)  =  (h2  <i>))  \mwedge{}  ((h1  ə-i>)  =  (h2  ə-i>)))
Date html generated:
2017_10_05-AM-01_00_22
Last ObjectModification:
2017_07_28-AM-09_25_44
Theory : cubical!type!theory
Home
Index