Nuprl Lemma : extd-nameset_subtype_int

`∀[L:Cname List]. (extd-nameset(L) ⊆r ℤ)`

Proof

Definitions occuring in Statement :  extd-nameset: `extd-nameset(L)` coordinate_name: `Cname` list: `T List` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` extd-nameset: `extd-nameset(L)` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` nameset: `nameset(L)` coordinate_name: `Cname` int_upper: `{i...}` int_seg: `{i..j-}`
Lemmas referenced :  extd-nameset_wf list_wf coordinate_name_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution imageElimination productElimination thin unionElimination equalityElimination sqequalRule setElimination rename hypothesisEquality hypothesis lemma_by_obid isectElimination axiomEquality

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

Date html generated: 2016_05_20-AM-09_29_01
Last ObjectModification: 2015_12_28-PM-04_48_02

Theory : cubical!sets

Home Index