Nuprl Definition : n-intersecting
n-intersecting(A;T;n) == ∀Ls:T List. ((||Ls|| = n ∈ ℤ) ⇒ (∃a:A. (∀L∈Ls.(a ∈ L))))
Definitions occuring in Statement :
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
length: ||as||,
list: T List,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
list: T List,
implies: P ⇒ Q,
equal: s = t ∈ T,
int: ℤ,
length: ||as||,
exists: ∃x:A. B[x],
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l)
FDL editor aliases :
n-intersecting
Latex:
n-intersecting(A;T;n) == \mforall{}Ls:T List. ((||Ls|| = n) {}\mRightarrow{} (\mexists{}a:A. (\mforall{}L\mmember{}Ls.(a \mmember{} L))))
Date html generated:
2016_05_15-PM-06_23_59
Last ObjectModification:
2015_09_23-AM-08_02_50
Theory : general
Home
Index