Nuprl Lemma : nerve-box-common-face_wf2

∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:cat-ob(poset-cat(I))]. ∀[z:nameset(I)].
  nerve-box-common-face(box;L;z) ∈ {f:I-face(cubical-nerve(C);I)| 
                                    (f ∈ box)
                                    ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)
                                    ∧ (direction(f) = (flip(L;z) dimension(f)) ∈ ℕ2)}  
  supposing (∃j∈J. ¬(j = z ∈ Cname)) ∨ (((L x) = i ∈ ℕ2) ∧ (¬↑null(J)))


Proof



Definitions occuring in Statement :  nerve-box-common-face: nerve-box-common-face(box;L;z),  cubical-nerve: cubical-nerve(X),  poset-cat: poset-cat(J),  open_box: open_box(X;I;J;x;i),  face-direction: direction(f),  face-dimension: dimension(f),  I-face: I-face(X;I),  name-morph-flip: flip(f;y),  nameset: nameset(L),  coordinate_name: Cname,  cat-ob: cat-ob(C),  small-category: SmallCategory,  l_exists: (∃x∈L. P[x]),  l_member: (x ∈ l),  null: null(as),  list: T List,  int_seg: {i..j-},  assert: ↑b,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  not: ¬A,  or: P ∨ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  natural_number: $n,  equal: s = t ∈ T
Definitions unfolded in proof :  poset-cat: poset-cat(J),  cat-ob: cat-ob(C),  pi1: fst(t),  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  open_box: open_box(X;I;J;x;i),  all: ∀x:A. B[x],  and: P ∧ Q,  subtype_rel: A ⊆r B,  name-morph: name-morph(I;J),  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  uiff: uiff(P;Q),  bfalse: ff,  prop: ℙ,  so_apply: x[s],  or: P ∨ Q,  int_seg: {i..j-},  nerve-box-common-face: nerve-box-common-face(box;L;z),  iff: P ⇐⇒ Q,  cand: A c∧ B,  so_lambda: λ2x.t[x],  nameset: nameset(L),  top: Top,  coordinate_name: Cname,  int_upper: {i...},  guard: {T},  lelt: i ≤ j < k,  decidable: Dec(P),  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  not: ¬A,  sq_stable: SqStable(P),  squash: ↓T,  rev_implies: P ⇐ Q,  l_exists: (∃x∈L. P[x]),  less_than: a < b,  I-face: I-face(X;I),  face-dimension: dimension(f),  face-direction: direction(f),  face-name: face-name(f),  pi2: snd(t),  sq_type: SQType(T),  name-morph-flip: flip(f;y),  bnot: ¬bb,  assert: ↑b,  true: True,  cons: [a / b],  le: A ≤ B
Lemmas referenced :  non_null_filter_iff,  I-face_wf,  cubical-nerve_wf,  eq_int_wf,  face-direction_wf,  face-dimension_wf,  bool_wf,  eqtt_to_assert,  assert_of_eq_int,  name-morph-flip_wf,  name-morph_wf,  nil_wf,  coordinate_name_wf,  equal_wf,  hd-wf-not-null,  filter_wf5,  l_member_wf,  int_seg_wf,  extd-nameset_subtype_int,  hd_member,  member_filter,  or_wf,  l_exists_wf,  nameset_wf,  not_wf,  assert_wf,  null_wf3,  subtype_rel_list,  top_wf,  open_box_wf,  list_wf,  small-category_wf,  int_seg_properties,  decidable__equal_int,  satisfiable-full-omega-tt,  intformand_wf,  intformnot_wf,  intformeq_wf,  itermVar_wf,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_eq_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  sq_stable__l_member,  decidable__equal-coordinate_name,  sq_stable__le,  decidable__le,  intformle_wf,  itermConstant_wf,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  decidable__lt,  intformless_wf,  int_formula_prop_less_lemma,  lelt_wf,  iff_transitivity,  iff_weakening_uiff,  assert_of_band,  l_exists_iff,  l_member_subtype,  extd-nameset-nil,  select_wf,  length_wf,  band_wf,  subtype_base_sq,  set_subtype_base,  int_subtype_base,  nameset_subtype_base,  le_wf,  eq-cname_wf,  assert-eq-cname,  and_wf,  pi1_wf_top,  eqff_to_assert,  bool_cases_sqequal,  bool_subtype_base,  assert-bnot,  list-cases,  null_nil_lemma,  product_subtype_list,  null_cons_lemma,  cons_member,  cons_wf,  subtype_rel_product,  pi2_wf,  equal-wf-base
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  sqequalTransitivity,  computationStep,  isect_memberFormation,  introduction,  cut,  sqequalHypSubstitution,  setElimination,  thin,  rename,  extract_by_obid,  isectElimination,  hypothesisEquality,  hypothesis,  dependent_functionElimination,  productElimination,  lambdaEquality,  applyEquality,  because_Cache,  lambdaFormation,  unionElimination,  equalityElimination,  independent_isectElimination,  equalityTransitivity,  equalitySymmetry,  independent_functionElimination,  natural_numberEquality,  setEquality,  dependent_set_memberEquality,  independent_pairFormation,  productEquality,  axiomEquality,  isect_memberEquality,  voidElimination,  voidEquality,  intEquality,  dependent_pairFormation,  int_eqEquality,  computeAll,  imageMemberEquality,  baseClosed,  imageElimination,  applyLambdaEquality,  independent_pairEquality,  promote_hyp,  instantiate,  cumulativity,  hyp_replacement,  hypothesis_subsumption,  inlFormation
Latex:
\mforall{}[C:SmallCategory].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(C);I;J;x;i)].  \mforall{}[L:cat-ob(poset-cat(I))].  \mforall{}[z:nameset(I)].
    nerve-box-common-face(box;L;z)  \mmember{}  \{f:I-face(cubical-nerve(C);I)| 
                                                                        (f  \mmember{}  box)
                                                                        \mwedge{}  (direction(f)  =  (L  dimension(f)))
                                                                        \mwedge{}  (direction(f)  =  (flip(L;z)  dimension(f)))\}   
    supposing  (\mexists{}j\mmember{}J.  \mneg{}(j  =  z))  \mvee{}  (((L  x)  =  i)  \mwedge{}  (\mneg{}\muparrow{}null(J)))


Date html generated: 2017_10_05-PM-03_36_46
Last ObjectModification: 2017_07_28-AM-11_25_19

Theory : cubical!sets


Home Index