Nuprl Lemma : mk-general-bounded-dist-lattice_wf

[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[E:T ⟶ T ⟶ ℙ].
  mk-general-bounded-dist-lattice(T;m;j;z;o;E) ∈ GeneralBoundedDistributiveLattice 
  supposing EquivRel(T;x,y.E y)
  ∧ (∀[a,b:T].  (E m[a;b] m[b;a]))
  ∧ (∀[a,b:T].  (E j[a;b] j[b;a]))
  ∧ (∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c]))
  ∧ (∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c]))
  ∧ (∀[a,b:T].  (E j[a;m[a;b]] a))
  ∧ (∀[a,b:T].  (E m[a;j[a;b]] a))
  ∧ (∀[a:T]. (E m[a;o] a))
  ∧ (∀[a:T]. (E j[a;z] a))
  ∧ (∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]]))


Proof




Definitions occuring in Statement :  mk-general-bounded-dist-lattice: mk-general-bounded-dist-lattice(T;m;j;z;o;E) general-bounded-distributive-lattice: GeneralBoundedDistributiveLattice equiv_rel: EquivRel(T;x,y.E[x; y]) uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] and: P ∧ Q member: t ∈ T apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q mk-general-bounded-dist-lattice: mk-general-bounded-dist-lattice(T;m;j;z;o;E) general-bounded-distributive-lattice: GeneralBoundedDistributiveLattice mk-general-bounded-lattice: mk-general-bounded-lattice(T;m;j;z;o;E) prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: λ2x.t[x] so_apply: x[s] general-bounded-lattice-structure: GeneralBoundedLatticeStructure record+: record+ record-update: r[x := v] record: record(x.T[x]) all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt subtype_rel: A ⊆B uiff: uiff(P;Q) ifthenelse: if then else fi  sq_type: SQType(T) guard: {T} record-select: r.x top: Top eq_atom: =a y bfalse: ff iff: ⇐⇒ Q not: ¬A rev_implies:  Q lattice-meet: a ∧ b lattice-join: a ∨ b lattice-point: Point(l) general-lattice-axioms: general-lattice-axioms(l) lattice-equiv: a ≡ b lattice-1: 1 lattice-0: 0 cand: c∧ B
Lemmas referenced :  equiv_rel_wf uall_wf eq_atom_wf uiff_transitivity equal-wf-base bool_wf assert_wf atom_subtype_base eqtt_to_assert assert_of_eq_atom subtype_base_sq rec_select_update_lemma iff_transitivity bnot_wf not_wf iff_weakening_uiff eqff_to_assert assert_of_bnot equal_wf general-lattice-axioms_wf lattice-point_wf bounded-lattice-structure-subtype general-bounded-lattice-structure-subtype subtype_rel_transitivity general-bounded-lattice-structure_wf bounded-lattice-structure_wf lattice-structure_wf lattice-equiv_wf lattice-meet_wf lattice-join_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin dependent_set_memberEquality hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry productEquality extract_by_obid isectElimination cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality because_Cache isect_memberEquality functionEquality universeEquality dependentIntersection_memberEquality tokenEquality lambdaFormation unionElimination equalityElimination baseApply closedConclusion baseClosed atomEquality independent_functionElimination independent_isectElimination instantiate dependent_functionElimination voidElimination voidEquality independent_pairFormation impliesFunctionality

Latex:
\mforall{}[T:Type].  \mforall{}[m,j:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[z,o:T].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    mk-general-bounded-dist-lattice(T;m;j;z;o;E)  \mmember{}  GeneralBoundedDistributiveLattice 
    supposing  EquivRel(T;x,y.E  x  y)
    \mwedge{}  (\mforall{}[a,b:T].    (E  m[a;b]  m[b;a]))
    \mwedge{}  (\mforall{}[a,b:T].    (E  j[a;b]  j[b;a]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (E  m[a;m[b;c]]  m[m[a;b];c]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (E  j[a;j[b;c]]  j[j[a;b];c]))
    \mwedge{}  (\mforall{}[a,b:T].    (E  j[a;m[a;b]]  a))
    \mwedge{}  (\mforall{}[a,b:T].    (E  m[a;j[a;b]]  a))
    \mwedge{}  (\mforall{}[a:T].  (E  m[a;o]  a))
    \mwedge{}  (\mforall{}[a:T].  (E  j[a;z]  a))
    \mwedge{}  (\mforall{}[a,b,c:T].    (E  m[a;j[b;c]]  j[m[a;b];m[a;c]]))



Date html generated: 2020_05_20-AM-08_58_41
Last ObjectModification: 2017_07_28-AM-09_18_03

Theory : lattices


Home Index