Nuprl Lemma : assert-face-name-eq
∀[I:Cname List]. ∀[a,b:nameset(I) × ℕ2]. uiff(↑face-name-eq(a;b);a = b ∈ (nameset(I) × ℕ2))
Proof
Definitions occuring in Statement :
face-name-eq: face-name-eq(a;b),
nameset: nameset(L),
coordinate_name: Cname,
list: T List,
int_seg: {i..j-},
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
product: x:A × B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
nameset: nameset(L),
face-name-eq: face-name-eq(a;b),
coordinate_name: Cname,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
all: ∀x:A. B[x],
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T},
prop: ℙ,
int_upper: {i...},
int_seg: {i..j-},
subtype_rel: A ⊆r B,
deq: EqDecider(T),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
subtype_base_sq,
product_subtype_base,
int_subtype_base,
equal_wf,
subtype_rel_product,
int_upper_wf,
l_member_wf,
int_seg_wf,
set_wf,
equal_functionality_wrt_subtype_rel2,
assert_wf,
product-deq_wf,
int-deq_wf,
uiff_wf,
deq_wf,
list_wf,
assert_witness,
iff_weakening_uiff,
assert-product-deq
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
independent_pairFormation,
isect_memberFormation,
cut,
thin,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
cumulativity,
productEquality,
intEquality,
independent_isectElimination,
because_Cache,
lambdaEquality,
hypothesis,
lambdaFormation,
dependent_functionElimination,
independent_functionElimination,
hypothesisEquality,
productElimination,
independent_pairEquality,
setElimination,
rename,
setEquality,
natural_numberEquality,
dependent_set_memberEquality,
applyEquality,
isect_memberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
addLevel
Latex:
\mforall{}[I:Cname List]. \mforall{}[a,b:nameset(I) \mtimes{} \mBbbN{}2]. uiff(\muparrow{}face-name-eq(a;b);a = b)
Date html generated:
2017_10_05-AM-10_17_30
Last ObjectModification:
2017_07_28-AM-11_20_20
Theory : cubical!sets
Home
Index