[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
. * .	real-multdiv	f	Real × Real → Real
. + .	int-basic2	f	Int × Int → Int
. + .	real-basic	f	Real × Real → Real
. + .	nat-basic	f	Nat × Nat → Nat
. +1	int-basic1	f	Int → Int
. +1	nat-basic	f	Nat → Nat
. - .	int-abs	f	Int × Int → Int
. - .	real-abs	f	Real × Real → Real
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	int-basic1	f	Int → Int
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. .r	real-basic	f	Int → Real
. / .	real-multdiv	pf	Real × Real → Real with λ r0, r. r ≠ 0.r
. < .	int-basic1	p	Int × Int
. < .	real-basic	p	Real × Real
. < .	nat-basic	p	Nat × Nat
. > .	int-abs	p	Int × Int
. > .	real-abs	p	Real × Real
. > .	nat	p	Nat × Nat
. ^-1	real-multdiv	pf	Real → Real with λ r. r ≠ 0.r
. ≤ .	int-abs	p	Int × Int
. ≤ .	real-abs	p	Real × Real
. ≤ .	real-supinf	p	(Real → Type(Bool)) × Real
. ≤ .	real-supinf	p	Real × (Real → Type(Bool))
. ≤ .	nat	p	Nat × Nat
. ≥ .	int-abs	p	Int × Int
. ≥ .	real-abs	p	Real × Real
. ≥ .	nat	p	Nat × Nat
~ .	int-abs	f	Int → Int
~ .	real-basic	f	Real → Real
ε	real-limit	v	Real
Int	int-basic1	s
Nat	nat-basic	s
Real	real-basic	s
abs	int-abs	f	Int → Int
abs	real-abs	f	Real → Real
bounded≤	real-supinf	p	(Real → Type(Bool))
bounded≤	real-limit	p	(Nat → Type(Real)) × Real
bounded≥	real-supinf	p	(Real → Type(Bool))
bounded≥	real-limit	p	(Nat → Type(Real)) × Real
converges	real-limit	p	(Nat → Type(Real))
converges	real-limit	p	(Nat → Type(Real)) × Real
f	real-limit	v	Nat → Real
i	real-limit	v	Int
inf	real-supinf	pf	(Real → Bool) → Real with λ rset. bounded≥(rset)
j	real-limit	v	Int
limit	real-limit	pf	(Nat → Real) → Real with λ f. converges(f)
max	real-min-max	f	Real × Real → Real
min	real-min-max	f	Real × Real → Real
mon≤	real-limit	p	(Nat → Type(Real))
mon≥	real-limit	p	(Nat → Type(Real))
n	real-limit	v	Nat
r	real-limit	v	Real
sup	real-supinf	pf	(Real → Bool) → Real with λ rset. bounded≤(rset)