Nuprl Definition : possible-majority
possible-majority(T;eq;L;x) == ∀y:T. (||L|| < 2 * count(eq y;L) ⇒ (y = x ∈ T))
Definitions occuring in Statement :
count: count(P;L),
length: ||as||,
less_than: a < b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
multiply: n * m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
less_than: a < b,
length: ||as||,
multiply: n * m,
natural_number: $n,
count: count(P;L),
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
possible-majority
Latex:
possible-majority(T;eq;L;x) == \mforall{}y:T. (||L|| < 2 * count(eq y;L) {}\mRightarrow{} (y = x))
Date html generated:
2016_05_14-PM-03_22_10
Last ObjectModification:
2015_09_22-PM-05_59_28
Theory : decidable!equality
Home
Index