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