Nuprl Definition : unique-minimal
unique-minimal(T;x,y.R[x; y];m) == (∀x:T. (¬R[x; m])) ∧ (∀y:T. ((∀x:T. (¬R[x; y])) ⇒ (y = m ∈ T)))
Definitions occuring in Statement :
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x],
not: ¬A,
equal: s = t ∈ T
FDL editor aliases :
unique-minimal
Latex:
unique-minimal(T;x,y.R[x; y];m) == (\mforall{}x:T. (\mneg{}R[x; m])) \mwedge{} (\mforall{}y:T. ((\mforall{}x:T. (\mneg{}R[x; y])) {}\mRightarrow{} (y = m)))
Date html generated:
2016_05_15-PM-07_50_15
Last ObjectModification:
2015_09_23-AM-08_18_57
Theory : general
Home
Index