Nuprl Definition : unique_set
{!x:T | P[x]} == {x:T| P[x] ∧ (∀y:T. (P[y] ⇒ (y = x ∈ T)))}
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
unique_set
Latex:
\{!x:T | P[x]\} == \{x:T| P[x] \mwedge{} (\mforall{}y:T. (P[y] {}\mRightarrow{} (y = x)))\}
Date html generated:
2016_05_13-PM-03_15_23
Last ObjectModification:
2016_01_04-AM-10_26_38
Theory : core_2
Home
Index