Nuprl Definition : discrete-type
discrete-type(T) == ∀f:ℝ ⟶ T. ((∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y) ∈ T))) ⇒ (∀x,y:ℝ. ((f x) = (f y) ∈ T)))
Definitions occuring in Statement :
req: x = y,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
function: x:A ⟶ B[x],
implies: P ⇒ Q,
req: x = y,
all: ∀x:A. B[x],
real: ℝ,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
discrete-type
Latex:
discrete-type(T) ==
\mforall{}f:\mBbbR{} {}\mrightarrow{} T. ((\mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((f x) = (f y)))) {}\mRightarrow{} (\mforall{}x,y:\mBbbR{}. ((f x) = (f y))))
Date html generated:
2018_05_22-PM-02_13_01
Last ObjectModification:
2017_10_27-PM-01_11_17
Theory : reals
Home
Index