Nuprl Lemma : subtype_rel_bunion
A,B:Type. ((A 
r B) 
((A 
B) r B))
Proof
Definitions occuring in Statement :
subtype_rel: A r B,
b-union: A B,
all: x:A. B[x],
implies: P Q,
universe: Type
Definitions :
all: x:A. B[x],
implies: P Q,
member: t 
T,
uall: [x:A]. B[x],
b-union: A B,
bool: 
,
ifthenelse: if b then t else f fi
Lemmas :
b-union_wf
\mforall{}A,B:Type. ((A \msubseteq{}r B) {}\mRightarrow{} ((A \mcup{} B) \msubseteq{}r B))
Date html generated:
2013_03_20-AM-09_45_57
Last ObjectModification:
2012_11_30-PM-03_40_20
Home
Index