### Nuprl Lemma : cube-set-restriction-face-map

`∀[X:CubicalSet]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[s:X(I)]. ∀[c:ℕ2]. ∀[j:name-morph-domain(f;I)].`
`  ((f j:=c)(f(s)) = f((j:=c)(s)) ∈ X(K-[f j]))`

Proof

Definitions occuring in Statement :  cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` face-map: `(x:=i)` name-morph-domain: `name-morph-domain(f;I)` name-morph: `name-morph(I;J)` cname_deq: `CnameDeq` coordinate_name: `Cname` list-diff: `as-bs` cons: `[a / b]` nil: `[]` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` apply: `f a` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` cubical-set: `CubicalSet` and: `P ∧ Q` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` guard: `{T}` nameset: `nameset(L)` I-cube: `X(I)` top: `Top` compose: `f o g` prop: `ℙ` squash: `↓T` cube-set-restriction: `f(s)` pi2: `snd(t)` name-morph-domain: `name-morph-domain(f;I)` ext-eq: `A ≡ B` uimplies: `b supposing a` true: `True` face-map: `(x:=i)` name-comp: `(f o g)` uext: `uext(g)` implies: `P `` Q` name-morph: `name-morph(I;J)` uiff: `uiff(P;Q)` coordinate_name: `Cname` int_upper: `{i...}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` false: `False` isname: `isname(z)` int_seg: `{i..j-}` decidable: `Dec(P)` le_int: `i ≤z j` lt_int: `i <z j` lelt: `i ≤ j < k` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` nequal: `a ≠ b ∈ T ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  name-morph_subtype_domain list-diff_wf coordinate_name_wf cname_deq_wf cons_wf nil_wf face-map_wf2 ob_pair_lemma istype-void name-morph-domain_wf int_seg_wf equal_wf squash_wf true_wf istype-universe nameset_wf list_wf name-morph-domain_subtype name-morph_subtype_remove1 name-morphs-equal name-comp_wf assert-isname eq_int_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_subtype_base bool_cases_sqequal subtype_base_sq bool_wf assert-bnot neg_assert_of_eq_int decidable__equal_int int_subtype_base int_seg_properties bfalse_wf int_seg_subtype_special int_seg_cases full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf nsub2_subtype_extd-nameset iff_imp_equal_bool le_int_wf btrue_wf iff_functionality_wrt_iff assert_wf le_wf iff_weakening_uiff assert_of_le_int iff_weakening_equal nameset_subtype_base member-list-diff intformeq_wf intformnot_wf int_formula_prop_eq_lemma int_formula_prop_not_lemma set_subtype_base member_singleton l_member_wf name-morph_wf false_wf istype-le isname-nameset eq_int_eq_true subtype_rel_self bnot_wf assert_elim btrue_neq_bfalse isname_wf extd-nameset_subtype_int equal-wf-T-base not_wf istype-assert uiff_transitivity iff_transitivity assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis setElimination rename productElimination dependent_functionElimination because_Cache equalityTransitivity equalitySymmetry lambdaEquality_alt inhabitedIsType sqequalRule isect_memberEquality_alt voidElimination universeIsType axiomEquality isectIsTypeImplies natural_numberEquality applyLambdaEquality hyp_replacement imageElimination instantiate universeEquality imageMemberEquality baseClosed lambdaEquality functionExtensionality voidEquality isect_memberEquality comment independent_isectElimination lambdaFormation_alt equalityIsType1 independent_functionElimination unionElimination equalityElimination dependent_pairFormation_alt equalityIsType3 promote_hyp cumulativity intEquality hypothesis_subsumption approximateComputation int_eqEquality independent_pairFormation dependent_set_memberEquality_alt equalityIsType2 closedConclusion productIsType baseApply equalityIsType4 functionIsType setEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,K:Cname  List].  \mforall{}[f:name-morph(I;K)].  \mforall{}[s:X(I)].  \mforall{}[c:\mBbbN{}2].
\mforall{}[j:name-morph-domain(f;I)].
((f  j:=c)(f(s))  =  f((j:=c)(s)))

Date html generated: 2019_11_05-PM-00_25_50
Last ObjectModification: 2018_11_08-PM-01_15_56

Theory : cubical!sets

Home Index