Nuprl Lemma : extended-face-map

I:Cname List. ∀x1,x2:nameset(I). ∀i:ℕ2. ∀y1,y2:Cname.
  (x2:=i)[y1:=y2] ((x2:=i) rename-one-name(y1;y2)) ∈ name-morph([y1 I-[x1]];[y2 I-[x1; x2]]) 
  supposing (y2 ∈ I-[x1; x2])) ∧ (y1 ∈ I))


Proof




Definitions occuring in Statement :  rename-one-name: rename-one-name(z1;z2) name-comp: (f g) face-map: (x:=i) extend-name-morph: f[z1:=z2] name-morph: name-morph(I;J) nameset: nameset(L) cname_deq: CnameDeq coordinate_name: Cname list-diff: as-bs l_member: (x ∈ l) cons: [a b] nil: [] 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 nameset: nameset(L) not: ¬A implies:  Q prop: false: False true: True subtype_rel: A ⊆B squash: T guard: {T} iff: ⇐⇒ Q rev_implies:  Q name-morph: name-morph(I;J) cand: c∧ B coordinate_name: Cname int_upper: {i...} so_lambda: λ2x.t[x] int_seg: {i..j-} lelt: i ≤ j < k less_than: a < b so_apply: x[s] sq_type: SQType(T) or: P ∨ Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] bnot: ¬bb assert: b rename-one-name: rename-one-name(z1;z2) face-map: (x:=i) name-comp: (f g) extend-name-morph: f[z1:=z2] compose: g uext: uext(g) isname: isname(z) le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) l_member: (x ∈ l) nat: less_than': less_than'(a;b) top: Top select: L[n] cons: [a b] nat_plus: + nequal: a ≠ b ∈  decidable: Dec(P) sq_stable: SqStable(P) ge: i ≥ 
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf list-diff_wf cname_deq_wf nil_wf extend-name-morph_wf l_member_wf istype-void int_seg_wf nameset_wf list_wf face-map_wf2 name-morph_wf subtype_rel_wf squash_wf true_wf istype-universe list-diff2 iff_weakening_equal subtype_rel_self name-comp_wf rename-one-name_wf member-list-diff subtype_base_sq list_subtype_base set_subtype_base le_wf istype-int int_subtype_base equal_wf list-diff-cons-single cons_member member_singleton list-diff-cons deq-member_wf eqtt_to_assert assert-deq-member eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot eq_int_wf assert_of_eq_int neg_assert_of_eq_int iff_imp_equal_bool le_int_wf bfalse_wf iff_functionality_wrt_iff assert_wf false_wf iff_weakening_uiff assert_of_le_int int_seg_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf istype-le eq-cname_wf assert-eq-cname equal-wf-T-base nsub2_subtype_extd-nameset isname-nameset nameset_subtype_extd-nameset length_of_cons_lemma add_nat_plus length_wf_nat decidable__lt intformnot_wf int_formula_prop_not_lemma istype-less_than nat_plus_properties add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma length_wf select_wf nat_properties sq_stable__le sq_stable__l_member decidable__equal-coordinate_name decidable__le nameset_subtype l_subset_right_cons_trivial
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt cut sqequalHypSubstitution productElimination thin introduction extract_by_obid isectElimination hypothesis hypothesisEquality setElimination rename because_Cache independent_isectElimination sqequalRule productIsType functionIsType universeIsType inhabitedIsType natural_numberEquality applyEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry instantiate universeEquality imageMemberEquality baseClosed independent_functionElimination dependent_functionElimination independent_pairFormation cumulativity intEquality equalityIstype hyp_replacement dependent_set_memberEquality_alt applyLambdaEquality voidElimination unionElimination inlFormation_alt inrFormation_alt equalityElimination dependent_pairFormation_alt promote_hyp functionExtensionality approximateComputation int_eqEquality Error :memTop,  isect_memberEquality_alt pointwiseFunctionality baseApply closedConclusion sqequalBase unionIsType

Latex:
\mforall{}I:Cname  List.  \mforall{}x1,x2:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}y1,y2:Cname.
    (x2:=i)[y1:=y2]  =  ((x2:=i)  o  rename-one-name(y1;y2))  supposing  (\mneg{}(y2  \mmember{}  I-[x1;  x2]))  \mwedge{}  (\mneg{}(y1  \mmember{}  I))



Date html generated: 2020_05_21-AM-10_49_28
Last ObjectModification: 2019_12_10-PM-00_44_07

Theory : cubical!sets


Home Index