Nuprl Lemma : mk-s-group_wf

∀[ss:SeparationSpace]. ∀[e:Point]. ∀[i:Point ⟶ Point]. ∀[o:{f:Point ⟶ Point ⟶ Point| 
                                                             (∀x,y,z:Point.  f x (f y z) ≡ f (f x y) z)
                                                             ∧ (∀x:Point. f x e ≡ x)
                                                             ∧ (∀x:Point. f x (i x) ≡ e)} ]. ∀[sep:∀x,x',y,y':Point.
                                                                                                    (o x y # o x' y
                                                                                                    ⇒ (x # x'
                                                                                                       ∨ y # y'))].
∀[invsep:∀x,y:Point.  (i x # i y ⇒ x # y)].
  (mk-s-group(ss; e; i; o; sep; invsep) ∈ s-Group)


Proof



Definitions occuring in Statement :  mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),  s-group: s-Group,  ss-eq: x ≡ y,  ss-sep: x # y,  ss-point: Point,  separation-space: SeparationSpace,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ⟶ B[x]
Definitions unfolded in proof :  record: record(x.T[x]),  ss-eq: x ≡ y,  rev_implies: P ⇐ Q,  not: ¬A,  iff: P ⇐⇒ Q,  bfalse: ff,  top: Top,  sq_type: SQType(T),  uimplies: b supposing a,  and: P ∧ Q,  uiff: uiff(P;Q),  it: ⋅,  unit: Unit,  bool: 𝔹,  record-update: r[x := v],  ss-point: Point,  ss-sep: x # y,  s-group: s-Group,  mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),  or: P ∨ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q,  so_apply: x[s],  so_lambda: λ2x.t[x],  prop: ℙ,  guard: {T},  btrue: tt,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  subtype_rel: A ⊆r B,  record-select: r.x,  record+: record+,  separation-space: SeparationSpace,  member: t ∈ T,  uall: ∀[x:A]. B[x]
Lemmas referenced :  separation-space_wf,  ss-eq_wf,  set_wf,  ss-sep_wf,  ss-point_wf,  assert_of_bnot,  eqff_to_assert,  iff_weakening_uiff,  bnot_wf,  iff_transitivity,  rec_select_update_lemma,  subtype_base_sq,  assert_of_eq_atom,  eqtt_to_assert,  atom_subtype_base,  assert_wf,  bool_wf,  equal-wf-base,  uiff_transitivity,  eq_atom_wf,  or_wf,  not_wf,  all_wf,  subtype_rel_self
Rules used in proof :  productEquality,  axiomEquality,  equalityEquality,  impliesFunctionality,  independent_pairFormation,  voidEquality,  voidElimination,  isect_memberEquality,  dependent_functionElimination,  independent_isectElimination,  productElimination,  independent_functionElimination,  atomEquality,  baseClosed,  closedConclusion,  baseApply,  equalityElimination,  unionElimination,  lambdaFormation,  dependentIntersection_memberEquality,  rename,  setElimination,  functionExtensionality,  because_Cache,  cumulativity,  lambdaEquality,  equalitySymmetry,  equalityTransitivity,  functionEquality,  setEquality,  universeEquality,  isectElimination,  extract_by_obid,  instantiate,  tokenEquality,  applyEquality,  hypothesis,  thin,  dependentIntersectionEqElimination,  sqequalRule,  dependentIntersectionElimination,  sqequalHypSubstitution,  hypothesisEquality,  cut,  introduction,  isect_memberFormation,  sqequalReflexivity,  computationStep,  sqequalTransitivity,  sqequalSubstitution
Latex:
\mforall{}[ss:SeparationSpace].  \mforall{}[e:Point].  \mforall{}[i:Point  {}\mrightarrow{}  Point].  \mforall{}[o:\{f:Point  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point| 
                                                                                                                          (\mforall{}x,y,z:Point.
                                                                                                                                f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                                                                                                                          \mwedge{}  (\mforall{}x:Point.  f  x  e  \mequiv{}  x)
                                                                                                                          \mwedge{}  (\mforall{}x:Point.  f  x  (i  x)  \mequiv{}  e)\}  ].
\mforall{}[sep:\mforall{}x,x',y,y':Point.    (o  x  y  \#  o  x'  y  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))].  \mforall{}[invsep:\mforall{}x,y:Point.
                                                                                                                                                        (i  x  \#  i  y  {}\mRightarrow{}  x  \#  y)].
    (mk-s-group(ss;  e;  i;  o;  sep;  invsep)  \mmember{}  s-Group)


Date html generated: 2016_11_08-AM-09_11_44
Last ObjectModification: 2016_11_02-PM-05_08_13

Theory : inner!product!spaces


Home Index