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