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