Nuprl Lemma : name-morph-flip-face-map1

`∀I:Cname List. ∀y:nameset(I). ∀a:ℕ2. ∀f:name-morph(I-[y];[]). ∀v:nameset(I).`
`  ((¬(v = y ∈ Cname)) `` (flip(((y:=a) o f);v) = ((y:=a) o flip(f;v)) ∈ name-morph(I;[])))`

Proof

Definitions occuring in Statement :  name-morph-flip: `flip(f;y)` name-comp: `(f o g)` face-map: `(x:=i)` name-morph: `name-morph(I;J)` nameset: `nameset(L)` cname_deq: `CnameDeq` coordinate_name: `Cname` list-diff: `as-bs` cons: `[a / b]` nil: `[]` list: `T List` int_seg: `{i..j-}` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` nameset: `nameset(L)` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` cand: `A c∧ B` not: `¬A` prop: `ℙ` false: `False` guard: `{T}` uimplies: `b supposing a` name-morph-flip: `flip(f;y)` face-map: `(x:=i)` name-comp: `(f o g)` compose: `f o g` uext: `uext(g)` coordinate_name: `Cname` int_upper: `{i...}` 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` decidable: `Dec(P)` or: `P ∨ Q` sq_type: `SQType(T)` isname: `isname(z)` le_int: `i ≤z j` lt_int: `i <z j` bnot: `¬bb` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` bfalse: `ff` squash: `↓T` less_than: `a < b` top: `Top` assert: `↑b` subtype_rel: `A ⊆r B` name-morph: `name-morph(I;J)` nequal: `a ≠ b ∈ T `
Lemmas referenced :  member-list-diff coordinate_name_wf cname_deq_wf cons_wf nil_wf member_singleton l_member_wf list-diff_wf istype-void name-morph-ext name-morph-flip_wf name-comp_wf face-map_wf2 name-morph_wf int_seg_wf nameset_wf list_wf eq_int_wf eqtt_to_assert assert_of_eq_int decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties 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 eq-cname_wf assert-eq-cname intformeq_wf intformnot_wf int_formula_prop_eq_lemma int_formula_prop_not_lemma istype-le eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal_wf nsub2_subtype_extd-nameset neg_assert_of_eq_int subtract_wf decidable__le itermSubtract_wf int_term_value_subtract_lemma decidable__lt istype-less_than isname-name
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality_alt hypothesisEquality introduction extract_by_obid isectElimination hypothesis dependent_functionElimination because_Cache productElimination independent_functionElimination independent_pairFormation universeIsType sqequalRule functionIsType equalityIstype independent_isectElimination natural_numberEquality inhabitedIsType unionElimination equalityElimination equalityTransitivity equalitySymmetry instantiate cumulativity intEquality hypothesis_subsumption approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  voidElimination applyLambdaEquality imageMemberEquality baseClosed imageElimination isect_memberEquality_alt promote_hyp applyEquality productIsType

Latex:
\mforall{}I:Cname  List.  \mforall{}y:nameset(I).  \mforall{}a:\mBbbN{}2.  \mforall{}f:name-morph(I-[y];[]).  \mforall{}v:nameset(I).
((\mneg{}(v  =  y))  {}\mRightarrow{}  (flip(((y:=a)  o  f);v)  =  ((y:=a)  o  flip(f;v))))

Date html generated: 2020_05_21-AM-10_50_01
Last ObjectModification: 2019_12_10-PM-02_23_58

Theory : cubical!sets

Home Index