Nuprl Lemma : two-intersection-one-intersection
∀A:Id List. ∀W:{a:Id| (a ∈ A)} List List. (two-intersection(A;W) ⇒ one-intersection(A;W))
Proof
Definitions occuring in Statement :
two-intersection: two-intersection(A;W),
one-intersection: one-intersection(A;W),
Id: Id,
l_member: (x ∈ l),
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]}
Lemmas :
l_member_wf,
select_wf,
sq_stable__le,
int_seg_wf,
length_wf,
two-intersection_wf,
list_wf,
Id_wf
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. (two-intersection(A;W) {}\mRightarrow{} one-intersection(A;W))
Date html generated:
2015_07_17-AM-11_28_56
Last ObjectModification:
2015_01_28-AM-01_34_59
Home
Index