### Nuprl Lemma : face-map_wf

[L:Cname List]. ∀[x:Cname]. ∀[p:ℕ2].  ((x:=p) ∈ name-morph([x L];L))

Proof

Definitions occuring in Statement :  face-map: (x:=i) name-morph: name-morph(I;J) coordinate_name: Cname cons: [a b] list: List int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T natural_number: \$n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T face-map: (x:=i) name-morph: name-morph(I;J) nameset: nameset(L) coordinate_name: Cname int_upper: {i...} all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False subtype_rel: A ⊆B iff: ⇐⇒ Q nequal: a ≠ b ∈  squash: T not: ¬A int_seg: {i..j-} lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top decidable: Dec(P) isname: isname(z) le_int: i ≤j lt_int: i <j le: A ≤ B less_than': less_than'(a;b) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  int_seg_wf coordinate_name_wf list_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int nsub2_subtype_extd-nameset l_member_wf nameset_subtype_extd-nameset cons_member int_seg_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf intformnot_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf nameset_wf cons_wf nil_wf decidable__equal_int int_subtype_base false_wf int_seg_subtype int_seg_cases intformless_wf itermConstant_wf intformle_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_le_lemma assert_wf isname_wf extd-nameset_wf extd-nameset_subtype_base all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality sqequalRule sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination thin natural_numberEquality isect_memberEquality hypothesisEquality because_Cache lambdaEquality setElimination rename lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination applyEquality applyLambdaEquality imageMemberEquality baseClosed imageElimination int_eqEquality intEquality voidEquality independent_pairFormation computeAll hypothesis_subsumption addEquality functionEquality functionExtensionality

Latex:
\mforall{}[L:Cname  List].  \mforall{}[x:Cname].  \mforall{}[p:\mBbbN{}2].    ((x:=p)  \mmember{}  name-morph([x  /  L];L))

Date html generated: 2017_10_05-AM-10_06_24
Last ObjectModification: 2017_07_28-AM-11_16_20

Theory : cubical!sets

Home Index