Nuprl Lemma : extend-name-morph-face-map

I,K:Cname List. ∀f:name-morph(I;K). ∀z,x:Cname. ∀i:ℕ2.
  (f[z:=x] (x:=i)) ((z:=i) f) ∈ name-morph([z I];K) supposing (x ∈ K)) ∧ (z ∈ I))


Proof




Definitions occuring in Statement :  name-comp: (f g) face-map: (x:=i) extend-name-morph: f[z1:=z2] name-morph: name-morph(I;J) coordinate_name: Cname l_member: (x ∈ l) cons: [a b] list: List int_seg: {i..j-} uimplies: supposing a all: x:A. B[x] not: ¬A and: P ∧ Q natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a and: P ∧ Q uall: [x:A]. B[x] member: t ∈ T not: ¬A implies:  Q prop: false: False subtype_rel: A ⊆B name-morph: name-morph(I;J) face-map: (x:=i) name-comp: (f g) extend-name-morph: f[z1:=z2] compose: g uext: uext(g) nameset: nameset(L) coordinate_name: Cname int_upper: {i...} nequal: a ≠ b ∈  squash: T guard: {T} int_seg: {i..j-} lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) bfalse: ff or: P ∨ Q sq_type: SQType(T) bnot: ¬bb ifthenelse: if then else fi  assert: b top: Top le: A ≤ B less_than: a < b decidable: Dec(P) sq_stable: SqStable(P) rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q isname: isname(z) true: True
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf name-comp_wf extend-name-morph_wf face-map_wf l_member_wf istype-void int_seg_wf name-morph_wf nameset_wf eq-cname_wf eq_int_wf int_seg_properties full-omega-unsat intformand_wf intformeq_wf itermVar_wf intformnot_wf istype-int int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int int_subtype_base decidable__equal_int istype-le assert-eq-cname bool_wf iff_weakening_uiff assert_wf equal-wf-T-base set_subtype_base le_wf iff_imp_equal_bool le_int_wf btrue_wf iff_functionality_wrt_iff true_wf assert_of_le_int iff_weakening_equal istype-true bfalse_wf false_wf intformle_wf itermConstant_wf intformless_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_less_lemma nsub2_subtype_extd-nameset isname-nameset cons_member isname_wf assert-isname extd-nameset_subtype_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt cut sqequalHypSubstitution productElimination thin introduction extract_by_obid isectElimination hypothesis hypothesisEquality independent_isectElimination sqequalRule productIsType functionIsType universeIsType natural_numberEquality inhabitedIsType because_Cache applyEquality lambdaEquality_alt setElimination rename functionExtensionality applyLambdaEquality imageMemberEquality baseClosed imageElimination independent_functionElimination voidElimination approximateComputation dependent_pairFormation_alt int_eqEquality dependent_functionElimination Error :memTop,  independent_pairFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry equalityIstype promote_hyp instantiate isect_memberEquality_alt cumulativity intEquality dependent_set_memberEquality_alt

Latex:
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}z,x:Cname.  \mforall{}i:\mBbbN{}2.
    (f[z:=x]  o  (x:=i))  =  ((z:=i)  o  f)  supposing  (\mneg{}(x  \mmember{}  K))  \mwedge{}  (\mneg{}(z  \mmember{}  I))



Date html generated: 2020_05_21-AM-10_49_02
Last ObjectModification: 2019_12_08-PM-07_06_29

Theory : cubical!sets


Home Index