### Nuprl Lemma : extend-face-map-same

`∀[I:Cname List]. ∀[x,y:Cname]. ∀[i:ℕ2].`
`  (x:=i)[y:=y] = (x:=i) ∈ name-morph([y / I];[y / I]-[x]) supposing (¬(y = x ∈ Cname)) ∧ (¬(y ∈ I))`

Proof

Definitions occuring in Statement :  face-map: `(x:=i)` extend-name-morph: `f[z1:=z2]` name-morph: `name-morph(I;J)` cname_deq: `CnameDeq` coordinate_name: `Cname` list-diff: `as-bs` l_member: `(x ∈ l)` cons: `[a / b]` nil: `[]` list: `T List` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` all: `∀x:A. B[x]` sq_type: `SQType(T)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` so_apply: `x[s]` so_lambda: `λ2x.t[x]` int_upper: `{i...}` coordinate_name: `Cname` name-morph: `name-morph(I;J)` face-map: `(x:=i)` extend-name-morph: `f[z1:=z2]` nameset: `nameset(L)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` bfalse: `ff` or: `P ∨ Q` bnot: `¬bb` assert: `↑b` decidable: `Dec(P)` cand: `A c∧ B` nequal: `a ≠ b ∈ T `
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf list-diff_wf cname_deq_wf nil_wf istype-void l_member_wf int_seg_wf list_wf member-list-diff face-map_wf2 extend-name-morph_wf iff_weakening_equal list-diff-cons-single true_wf squash_wf equal_wf int_subtype_base le_wf set_subtype_base list_subtype_base subtype_base_sq name-morph_wf eq_int_wf eqtt_to_assert assert_of_eq_int eq-cname_wf assert-eq-cname 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 eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal-wf-T-base neg_assert_of_eq_int nameset_wf decidable__equal_int istype-le nsub2_subtype_extd-nameset nameset_subtype_extd-nameset not_wf member_singleton cons_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution productElimination thin extract_by_obid isectElimination hypothesis hypothesisEquality independent_isectElimination sqequalRule productIsType functionIsType equalityIstype inhabitedIsType universeIsType isect_memberEquality_alt axiomEquality isectIsTypeImplies natural_numberEquality lambdaFormation dependent_functionElimination independent_functionElimination baseClosed imageMemberEquality because_Cache universeEquality equalitySymmetry equalityTransitivity imageElimination applyEquality lambdaEquality intEquality cumulativity instantiate rename setElimination functionExtensionality lambdaFormation_alt unionElimination equalityElimination applyLambdaEquality approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality voidElimination independent_pairFormation promote_hyp Error :memTop,  dependent_set_memberEquality_alt dependent_set_memberEquality impliesFunctionality addLevel inlFormation

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:Cname].  \mforall{}[i:\mBbbN{}2].    (x:=i)[y:=y]  =  (x:=i)  supposing  (\mneg{}(y  =  x))  \mwedge{}  (\mneg{}(y  \mmember{}  I))

Date html generated: 2020_05_21-AM-10_48_56
Last ObjectModification: 2019_12_10-PM-00_09_02

Theory : cubical!sets

Home Index