### Nuprl Lemma : groupoid-nerve-filler2_wf

`∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)].`
`  groupoid-nerve-filler2(cat(G);I;J;box) ∈ cubical-nerve(cat(G))(I) supposing 3 < ||box||`

Proof

Definitions occuring in Statement :  groupoid-nerve-filler2: `groupoid-nerve-filler2(C;I;J;box)` cubical-nerve: `cubical-nerve(X)` open_box: `open_box(X;I;J;x;i)` I-cube: `X(I)` nameset: `nameset(L)` coordinate_name: `Cname` groupoid-cat: `cat(G)` groupoid: `Groupoid` length: `||as||` list: `T List` int_seg: `{i..j-}` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` l_exists: `(∃x∈L. P[x])` exists: `∃x:A. B[x]` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` guard: `{T}` int_seg: `{i..j-}` nameset: `nameset(L)` false: `False` coordinate_name: `Cname` int_upper: `{i...}` lelt: `i ≤ j < k` and: `P ∧ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` prop: `ℙ` cons: `[a / b]` bfalse: `ff` open_box: `open_box(X;I;J;x;i)` subtype_rel: `A ⊆r B` groupoid-nerve-filler2: `groupoid-nerve-filler2(C;I;J;box)` decidable: `Dec(P)` name-morph: `name-morph(I;J)` groupoid-cat: `cat(G)`
Lemmas referenced :  groupoid-edges-commute assert_wf not_wf and_wf nerve_box_edge_wf equal-wf-T-base nil_wf name-morph_wf extd-nameset-nil equal_wf top_wf null_wf3 decidable__assert nerve_box_label_wf poset_functor_extend-is-functor cubical-nerve-I-cube groupoid_wf list_wf int_seg_wf coordinate_name_wf subtype_rel_list open_box_wf I-face_wf length_wf less_than_wf false_wf null_cons_lemma product_subtype_list int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf itermConstant_wf itermVar_wf intformless_wf intformand_wf satisfiable-full-omega-tt int_seg_properties length_of_nil_lemma base_wf stuck-spread null_nil_lemma list-cases nameset_wf groupoid-cat_wf cubical-nerve_wf length-open_box-ge-3
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_functionElimination independent_functionElimination unionElimination sqequalRule productElimination baseClosed independent_isectElimination lambdaFormation isect_memberEquality voidElimination voidEquality natural_numberEquality because_Cache setElimination rename dependent_pairFormation lambdaEquality int_eqEquality intEquality independent_pairFormation computeAll promote_hyp hypothesis_subsumption axiomEquality equalityTransitivity equalitySymmetry applyEquality inlFormation inrFormation dependent_set_memberEquality setEquality

Latex:
\mforall{}[G:Groupoid].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(cat(G));I;J;x;i)].
groupoid-nerve-filler2(cat(G);I;J;box)  \mmember{}  cubical-nerve(cat(G))(I)  supposing  3  <  ||box||

Date html generated: 2016_06_16-PM-07_13_48
Last ObjectModification: 2016_01_18-PM-04_47_19

Theory : cubical!sets

Home Index