Nuprl Definition : ex-approx
ex-approx(e;t;t') == ∀f:Base. (e#f:Base ⇒ (f t?e:v.⊥ ≤ f t'?e:v.⊥))
Definitions occuring in Statement :
bottom: ⊥,
free-from-atom: a#x:T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
base: Base,
sqle: s ≤ t
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
free-from-atom: a#x:T,
base: Base,
sqle: s ≤ t,
apply: f a,
bottom: ⊥
FDL editor aliases :
ex-approx
Latex:
ex-approx(e;t;t') == \mforall{}f:Base. (e\#f:Base {}\mRightarrow{} (f t?e:v.\mbot{} \mleq{} f t'?e:v.\mbot{}))
Date html generated:
2017_02_20-AM-10_56_40
Last ObjectModification:
2017_01_19-PM-05_07_16
Theory : minimal-first-order-logic
Home
Index