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]}
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
two-intersection: two-intersection(A;W),
one-intersection: one-intersection(A;W),
l_all: (∀x∈L.P[x]),
member: t ∈ T,
exists: ∃x:A. B[x],
and: P ∧ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
int_seg: {i..j-},
uimplies: b supposing a,
guard: {T},
lelt: i ≤ j < k,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
not: ¬A,
top: Top,
less_than: a < b,
squash: ↓T
Latex:
\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:
2016_05_16-PM-00_01_26
Last ObjectModification:
2016_01_17-PM-03_51_07
Theory : event-ordering
Home
Index