### Nuprl Lemma : name-morph-decomp

`∀I,J:Cname List. ∀f:name-morph(I;J).`
`  ∃L:(Cname × ℕ2) List`
`   ∃K:Cname List`
`    (nameset(I) ≡ nameset(map(λp.(fst(p));L) @ K)`
`    ∧ (∃g:nameset(K) ⟶ nameset(J)`
`        (Inj(nameset(K);nameset(J);g) ∧ (f = (face-maps-comp(L) o degeneracy-map(g)) ∈ name-morph(I;J)))))`

Proof

Definitions occuring in Statement :  face-maps-comp: `face-maps-comp(L)` name-comp: `(f o g)` degeneracy-map: `degeneracy-map(f)` name-morph: `name-morph(I;J)` nameset: `nameset(L)` coordinate_name: `Cname` map: `map(f;as)` append: `as @ bs` list: `T List` inject: `Inj(A;B;f)` int_seg: `{i..j-}` ext-eq: `A ≡ B` pi1: `fst(t)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` nameset: `nameset(L)` name-morph: `name-morph(I;J)` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` pi1: `fst(t)` subtype_rel: `A ⊆r B` top: `Top` guard: `{T}` so_apply: `x[s]` mapfilter: `mapfilter(f;P;L)` compose: `f o g` ext-eq: `A ≡ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` bfalse: `ff` or: `P ∨ Q` cand: `A c∧ B` true: `True` sq_type: `SQType(T)` false: `False` name-morph-domain: `name-morph-domain(f;I)` degeneracy-map: `degeneracy-map(f)` name-comp: `(f o g)` uext: `uext(g)` l_subset: `l_subset(T;as;bs)` squash: `↓T` not: `¬A` int_seg: `{i..j-}` l_member: `(x ∈ l)` coordinate_name: `Cname` int_upper: `{i...}` nat: `ℕ` sq_stable: `SqStable(P)` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` outl: `outl(x)`
Lemmas referenced :  name-morph_wf list_wf coordinate_name_wf mapfilter_wf nameset_wf list-subtype bnot_wf isname_wf int_seg_wf assert_of_bnot not-assert-isname assert_wf exists_wf ext-eq_wf append_wf map_wf inject_wf equal_wf name-comp_wf face-maps-comp_wf name-morph_subtype pi1_wf_top subtype_rel_weakening degeneracy-map_wf map-map map-id filter_wf_top filter_wf5 l_member_wf member_append bool_wf eqtt_to_assert false_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot member_filter_2 or_wf assert-isname name-morph-domain-inject all_wf extd-nameset_wf face-maps-comp-property nameset_subtype ext-eq_inversion subtype_rel_transitivity squash_wf true_wf iff_weakening_equal set_subtype_base lelt_wf int_subtype_base cname_deq_wf strong-subtype-deq-subtype strong-subtype-set2 apply-alist-function subtype_rel_list top_wf le_wf select_wf sq_stable__le nat_properties sq_stable__l_member decidable__equal-coordinate_name decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf less_than_wf length_wf unit_wf2 union_subtype_base extd-nameset_subtype_base unit_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache equalityTransitivity equalitySymmetry lambdaEquality applyEquality setElimination rename productEquality natural_numberEquality sqequalRule productElimination independent_isectElimination independent_pairEquality setEquality dependent_pairFormation functionEquality functionExtensionality isect_memberEquality voidElimination voidEquality independent_pairFormation dependent_set_memberEquality dependent_functionElimination independent_functionElimination unionElimination equalityElimination inrFormation promote_hyp instantiate cumulativity inlFormation addLevel orFunctionality imageElimination universeEquality imageMemberEquality baseClosed intEquality applyLambdaEquality int_eqEquality computeAll unionEquality

Latex:
\mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).
\mexists{}L:(Cname  \mtimes{}  \mBbbN{}2)  List
\mexists{}K:Cname  List
(nameset(I)  \mequiv{}  nameset(map(\mlambda{}p.(fst(p));L)  @  K)
\mwedge{}  (\mexists{}g:nameset(K)  {}\mrightarrow{}  nameset(J)
(Inj(nameset(K);nameset(J);g)  \mwedge{}  (f  =  (face-maps-comp(L)  o  degeneracy-map(g))))))

Date html generated: 2017_10_05-AM-10_10_40
Last ObjectModification: 2017_07_28-AM-11_17_34

Theory : cubical!sets

Home Index