### Nuprl Lemma : rename-one-iota

`∀I:Cname List. ∀z,z1:Cname.`
`  (iota(z) o rename-one-name(z;z1)) = iota(z1) ∈ name-morph(I;[z1 / I]) supposing (¬(z1 ∈ I)) ∧ (¬(z ∈ I))`

Proof

Definitions occuring in Statement :  rename-one-name: `rename-one-name(z1;z2)` name-comp: `(f o g)` iota: `iota(x)` name-morph: `name-morph(I;J)` coordinate_name: `Cname` l_member: `(x ∈ l)` cons: `[a / b]` list: `T List` uimplies: `b supposing a` all: `∀x:A. B[x]` not: `¬A` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B` cand: `A c∧ B` name-morph: `name-morph(I;J)` rename-one-name: `rename-one-name(z1;z2)` iota: `iota(x)` name-comp: `(f o g)` compose: `f o g` uext: `uext(g)` ifthenelse: `if b then t else f fi ` btrue: `tt` nameset: `nameset(L)` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` coordinate_name: `Cname` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf iota_wf not_wf l_member_wf list_wf name-comp_wf rename-one-name_wf name-morph_wf isname-nameset eq-cname_wf bool_wf eqtt_to_assert assert-eq-cname eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot nameset_wf set_subtype_base le_wf int_subtype_base nameset_subtype l_subset_right_cons_trivial nameset_subtype_extd-nameset
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut sqequalHypSubstitution productElimination thin equalitySymmetry introduction extract_by_obid isectElimination hypothesisEquality hypothesis independent_isectElimination productEquality applyEquality sqequalRule independent_pairFormation lambdaEquality setElimination rename functionExtensionality unionElimination equalityElimination equalityTransitivity dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination because_Cache voidElimination intEquality natural_numberEquality

Latex:
\mforall{}I:Cname  List.  \mforall{}z,z1:Cname.
(iota(z)  o  rename-one-name(z;z1))  =  iota(z1)  supposing  (\mneg{}(z1  \mmember{}  I))  \mwedge{}  (\mneg{}(z  \mmember{}  I))

Date html generated: 2017_10_05-AM-10_09_20
Last ObjectModification: 2017_07_28-AM-11_17_11

Theory : cubical!sets

Home Index