Nuprl Definition : req*
x = y == ∃n:ℕ. ∀m:{n...}. ((x m) = (y m))
Definitions occuring in Statement :
req: x = y,
int_upper: {i...},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
all: ∀x:A. B[x],
int_upper: {i...},
req: x = y,
apply: f a
FDL editor aliases :
req*
Latex:
x = y == \mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. ((x m) = (y m))
Date html generated:
2018_05_22-PM-03_14_02
Last ObjectModification:
2017_10_06-PM-01_53_05
Theory : reals_2
Home
Index