Nuprl Lemma : free-dl_wf

`∀[X:Type]. (free-dl(X) ∈ BoundedDistributiveLattice)`

Proof

Definitions occuring in Statement :  free-dl: `free-dl(X)` bdd-distributive-lattice: `BoundedDistributiveLattice` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` free-dl: `free-dl(X)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` free-dl-type: `free-dl-type(X)` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` quotient: `x,y:A//B[x; y]` squash: `↓T` true: `True` guard: `{T}` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` dlattice-eq: `dlattice-eq(X;as;bs)` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` l_subset: `l_subset(T;as;bs)` or: `P ∨ Q` free-dl-join: `free-dl-join(as;bs)` top: `Top` trans: `Trans(T;x,y.E[x; y])` free-dl-meet: `free-dl-meet(as;bs)` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  dlattice-eq-equiv mk-bounded-distributive-lattice_wf free-dl-type_wf free-dl-meet_wf free-dl-join_wf nil_wf list_wf subtype_quotient dlattice-eq_wf cons_wf quotient-member-eq free-dl-meet_wf_list equal-wf-base equal_wf squash_wf true_wf exists_wf l_member_wf append_wf all_wf l_subset_wf member-free-dl-meet dlattice-order-iff dlattice-order_wf length_wf_nat nat_wf l_subset_append member_append equiv_rel_functionality_wrt_iff append_assoc l_subset_append2 l_subset_refl iff_weakening_equal list_accum_cons_lemma list_ind_nil_lemma list_accum_nil_lemma list_induction map_wf map_nil_lemma map_cons_lemma append-nil subtype_rel_list top_wf or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule cumulativity hypothesis lambdaEquality because_Cache independent_isectElimination isect_memberEquality axiomEquality independent_pairFormation universeEquality applyEquality promote_hyp lambdaFormation equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination pointwiseFunctionality pertypeElimination productElimination productEquality imageElimination natural_numberEquality imageMemberEquality baseClosed functionEquality addLevel impliesFunctionality allFunctionality existsFunctionality andLevelFunctionality dependent_pairFormation dependent_set_memberEquality hyp_replacement applyLambdaEquality setElimination rename inrFormation inlFormation unionElimination levelHypothesis existsLevelFunctionality voidElimination voidEquality equalityUniverse orFunctionality orLevelFunctionality

Latex:
\mforall{}[X:Type].  (free-dl(X)  \mmember{}  BoundedDistributiveLattice)

Date html generated: 2017_10_05-AM-00_32_26
Last ObjectModification: 2017_07_28-AM-09_13_28

Theory : lattices

Home Index