### Nuprl Lemma : face-name-eq_wf

`∀[I:Cname List]. ∀[a,b:nameset(I) × ℕ2].  (face-name-eq(a;b) ∈ 𝔹)`

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-}` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` product: `x:A × B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` face-name-eq: `face-name-eq(a;b)` subtype_rel: `A ⊆r B` nameset: `nameset(L)` coordinate_name: `Cname` int_upper: `{i...}` int_seg: `{i..j-}`
Lemmas referenced :  product-deq_wf int-deq_wf nameset_wf int_seg_wf list_wf coordinate_name_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality because_Cache hypothesis productElimination independent_pairEquality setElimination rename hypothesisEquality axiomEquality equalityTransitivity equalitySymmetry productEquality natural_numberEquality isect_memberEquality

Latex:
\mforall{}[I:Cname  List].  \mforall{}[a,b:nameset(I)  \mtimes{}  \mBbbN{}2].    (face-name-eq(a;b)  \mmember{}  \mBbbB{})

Date html generated: 2016_06_16-PM-05_49_24
Last ObjectModification: 2015_12_28-PM-04_31_19

Theory : cubical!sets

Home Index