### 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: List int_seg: {i..j-} uall: [x:A]. B[x] apply: a natural_number: \$n equal: 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 ⊆B guard: {T} nameset: nameset(L) I-cube: X(I) top: Top compose: 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: supposing a true: True face-map: (x:=i) name-comp: (f g) uext: uext(g) implies:  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 then else 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 ≤j lt_int: i <j lelt: i ≤ j < k not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) iff: ⇐⇒ Q rev_implies:  Q cand: c∧ B nequal: a ≠ b ∈  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