Nuprl Lemma : three-intersection-two-intersection
∀A:Id List. ∀W:{a:Id| (a ∈ A)} List List. (three-intersection(A;W) ⇒ two-intersection(A;W))
Proof
Definitions occuring in Statement :
three-intersection: three-intersection(A;W),
two-intersection: two-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,
three-intersection_wf,
list_wf,
Id_wf
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. (three-intersection(A;W) {}\mRightarrow{} two-intersection(A;W))
Date html generated:
2015_07_17-AM-11_28_51
Last ObjectModification:
2015_01_28-AM-01_35_14
Home
Index