Nuprl Lemma : bag-rep-is-single-valued
∀[A:Type]. ∀[n:ℕ]. ∀[a:A]. single-valued-bag(bag-rep(n;a);A)
Proof
Definitions occuring in Statement :
nat: ℕ,
uall: ∀[x:A]. B[x],
universe: Type,
single-valued-bag: single-valued-bag(b;T),
bag-rep: bag-rep(n;x)
Definitions unfolded in proof :
single-valued-bag: single-valued-bag(b;T),
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B
Latex:
\mforall{}[A:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[a:A]. single-valued-bag(bag-rep(n;a);A)
Date html generated:
2016_05_17-AM-11_10_09
Last ObjectModification:
2015_12_29-PM-05_15_34
Theory : process-model
Home
Index