Nuprl Lemma : nsub2_subtype_extd-nameset

[L:Cname List]. (ℕ2 ⊆extd-nameset(L))


Proof




Definitions occuring in Statement :  extd-nameset: extd-nameset(L) coordinate_name: Cname list: List int_seg: {i..j-} subtype_rel: A ⊆B uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  extd-nameset: extd-nameset(L) uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B
Lemmas referenced :  subtype_rel_b-union-right nameset_wf int_seg_wf list_wf coordinate_name_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality axiomEquality

Latex:
\mforall{}[L:Cname  List].  (\mBbbN{}2  \msubseteq{}r  extd-nameset(L))



Date html generated: 2016_05_20-AM-09_29_07
Last ObjectModification: 2015_12_28-PM-04_47_50

Theory : cubical!sets


Home Index