Nuprl Lemma : groupoid-nerve-filler1_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-filler1(G;I;J;x;i;box) ∈ cubical-nerve(cat(G))(I) supposing (¬↑null(J)) ∧ (||box|| ≤ 3)`

Proof

Definitions occuring in Statement :  groupoid-nerve-filler1: `groupoid-nerve-filler1(G;I;J;x;i;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||` null: `null(as)` list: `T List` int_seg: `{i..j-}` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` not: `¬A` and: `P ∧ Q` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` top: `Top` open_box: `open_box(X;I;J;x;i)` nameset: `nameset(L)` groupoid-nerve-filler1: `groupoid-nerve-filler1(G;I;J;x;i;box)` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` false: `False` guard: `{T}` name-morph: `name-morph(I;J)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` cons: `[a / b]` bfalse: `ff` nat: `ℕ` int_seg: `{i..j-}` le: `A ≤ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` lelt: `i ≤ j < k` subtract: `n - m` less_than': `less_than'(a;b)` listp: `A List+` groupoid-cat: `cat(G)`
Lemmas referenced :  length-open_box-le-3 cubical-nerve_wf groupoid-cat_wf not_wf assert_wf null_wf3 subtype_rel_list nameset_wf top_wf le_wf length_wf I-face_wf open_box_wf coordinate_name_wf int_seg_wf list_wf groupoid_wf cubical-nerve-I-cube poset_functor_extend-is-functor nerve_box_label_wf decidable__assert equal_wf extd-nameset-nil name-morph_wf nil_wf equal-wf-T-base nerve_box_edge1_wf hd_wf listp_properties list-cases length_of_nil_lemma null_nil_lemma product_subtype_list length_of_cons_lemma null_cons_lemma length_wf_nat nat_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel less_than_wf cat-arrow_wf name-morph-flip_wf groupoid-edges-commute1 hd_member list-subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin extract_by_obid isectElimination hypothesisEquality hypothesis dependent_functionElimination independent_functionElimination sqequalRule axiomEquality equalityTransitivity equalitySymmetry productEquality applyEquality independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache setElimination rename natural_numberEquality unionElimination inlFormation inrFormation lambdaFormation baseClosed promote_hyp hypothesis_subsumption addEquality independent_pairFormation intEquality minusEquality 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-filler1(G;I;J;x;i;box)  \mmember{}  cubical-nerve(cat(G))(I)
supposing  (\mneg{}\muparrow{}null(J))  \mwedge{}  (||box||  \mleq{}  3)

Date html generated: 2017_10_05-PM-03_43_44
Last ObjectModification: 2017_07_28-AM-11_27_08

Theory : cubical!sets

Home Index