mathcomp.analysis.altreals.distr

Global Index

_

(33778 entries)

Notation Index

A

G

H

J

K

O

Q

V

X

Y

Z

_

(623 entries)

Binder Index

_

(24219 entries)

Module Index

A

G

H

I

J

L

M

O

Q

V

W

X

Y

Z

_

other

(66 entries)

Variable Index

K

Q

V

X

Y

_

other

(1479 entries)

Library Index

A

G

H

I

J

K

O

Q

U

V

W

Y

Z

_

other

(34 entries)

Lemma Index

_

other

(4547 entries)

Constructor Index

A

G

H

J

M

Q

V

Y

Z

_

other

(98 entries)

Axiom Index

A

B

D

E

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Inductive Index

A

G

H

J

Q

R

V

W

Y

Z

_

other

(31 entries)

Projection Index

A

G

H

J

K

O

Q

V

W

X

Y

Z

_

other

(93 entries)

Section Index

K

Q

V

X

Y

_

other

(657 entries)

Instance Index

C

H

J

K

L

M

O

Q

R

V

X

Y

Z

_

other

(73 entries)

Abbreviation Index

J

K

W

Y

Z

_

other

(206 entries)

Definition Index

_

other

(1592 entries)

Record Index

A

G

H

J

K

O

Q

V

W

X

Y

Z

_

other

(55 entries)

other

\big [ _ / _ ]_ ( _ \in _ ) _ (big_scope) [notation, in mathcomp.analysis.fsbigop]
\big [ _ / _ ]_ ( _ \in _ ) _ (big_scope) [notation, in mathcomp.analysis.fsbigop]
\big [ _ / _ ]_ ( _ <oo ) _ (big_scope) [notation, in mathcomp.analysis.sequences]
\big [ _ / _ ]_ ( _ <oo | _ ) _ (big_scope) [notation, in mathcomp.analysis.sequences]
\big [ _ / _ ]_ ( _ <= _ <oo ) _ (big_scope) [notation, in mathcomp.analysis.sequences]
\big [ _ / _ ]_ ( _ <= _ <oo | _ ) _ (big_scope) [notation, in mathcomp.analysis.sequences]
`[< _ >] (bool_scope) [notation, in mathcomp.analysis.boolp]
_ #!= _ (card_scope) [notation, in mathcomp.analysis.cardinality]
_ #= _ (card_scope) [notation, in mathcomp.analysis.cardinality]
_ #>= _ (card_scope) [notation, in mathcomp.analysis.cardinality]
_ #<= _ (card_scope) [notation, in mathcomp.analysis.cardinality]
_ .-prod.-measurable (classical_set_scope) [notation, in mathcomp.analysis.measure]
_ .-cara.-measurable (classical_set_scope) [notation, in mathcomp.analysis.measure]
_ .-caratheodory (classical_set_scope) [notation, in mathcomp.analysis.measure]
_ .-ring.-measurable (classical_set_scope) [notation, in mathcomp.analysis.measure]
_ .-sigma.-measurable (classical_set_scope) [notation, in mathcomp.analysis.measure]
'measurable (classical_set_scope) [notation, in mathcomp.analysis.measure]
_ .-measurable (classical_set_scope) [notation, in mathcomp.analysis.measure]
<<r _ >> (classical_set_scope) [notation, in mathcomp.analysis.measure]
<<s _ >> (classical_set_scope) [notation, in mathcomp.analysis.measure]
<<s _ , _ >> (classical_set_scope) [notation, in mathcomp.analysis.measure]
<<d _ >> (classical_set_scope) [notation, in mathcomp.analysis.measure]
<<m _ >> (classical_set_scope) [notation, in mathcomp.analysis.measure]
<<m _ , _ >> (classical_set_scope) [notation, in mathcomp.analysis.measure]
_ @`] _ , _ [ (classical_set_scope) [notation, in mathcomp.analysis.normedtype]
_ @`[ _ , _ ] (classical_set_scope) [notation, in mathcomp.analysis.normedtype]
_ .-ocitv.-measurable (classical_set_scope) [notation, in mathcomp.analysis.lebesgue_measure]
{ family _ , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ ptws , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ ptws , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ uniform , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ uniform _ , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ uniform , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ uniform _ , _ --> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ uniform _ -> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
{ uniform` _ -> _ } (classical_set_scope) [notation, in mathcomp.analysis.topology]
to_set _ _ (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ ^-1 (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ \o _ (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ ^' (classical_set_scope) [notation, in mathcomp.analysis.topology]
\oo (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ ^° (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ `@ _ (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ `@[ _ --> _ ] (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ @ _ (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ @[ _ --> _ ] (classical_set_scope) [notation, in mathcomp.analysis.topology]
[ cvg _ in _ ] (classical_set_scope) [notation, in mathcomp.analysis.topology]
[ lim _ in _ ] (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ --> _ (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ `=>` _ (classical_set_scope) [notation, in mathcomp.analysis.topology]
[ filter of _ ] (classical_set_scope) [notation, in mathcomp.analysis.topology]
_ `#` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`] -oo , +oo [ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`] _ , +oo [ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`[ _ , +oo [ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`] -oo , _ [ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`] -oo , _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`] _ , _ [ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`[ _ , _ [ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`] _ , _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
`[ _ , _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set` _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ !=set0 (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ @` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ @^-1` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `<=>` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `<` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `<=` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\bigcap_ _ _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\bigcap_ ( _ : _ ) _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\bigcap_ ( _ in _ ) _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\bigcup_ _ _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\bigcup_ ( _ : _ ) _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\bigcup_ ( _ in _ ) _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ disjoint _ & _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `\ _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `\` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set ~ _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
~` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ ``*` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `*`` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ .`2 (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ .`1 (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `*` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `&` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ ; _ ; .. ; _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ |` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
_ `|` _ (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set : _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ : _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ | _ in _ & _ in _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ | _ in _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ | _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
[ set _ : _ | _ ] (classical_set_scope) [notation, in mathcomp.analysis.classical_sets]
\sum_ ( _ \in _ ) _ (ereal_scope) [notation, in mathcomp.analysis.fsbigop]
_ ^\- (ereal_scope) [notation, in mathcomp.analysis.numfun]
_ ^\+ (ereal_scope) [notation, in mathcomp.analysis.numfun]
\int [ _ ]_ _ _ (ereal_scope) [notation, in mathcomp.analysis.lebesgue_integral]
\int [ _ ]_ ( _ in _ ) _ (ereal_scope) [notation, in mathcomp.analysis.lebesgue_integral]
[ series _ ]_ _ (ereal_scope) [notation, in mathcomp.analysis.sequences]
\sum_ ( _ <oo ) _ (ereal_scope) [notation, in mathcomp.analysis.sequences]
\sum_ ( _ <oo | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.sequences]
\sum_ ( _ <= _ <oo ) _ (ereal_scope) [notation, in mathcomp.analysis.sequences]
\sum_ ( _ <= _ <oo | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.sequences]
[ sequence _ ]_ _ (ereal_scope) [notation, in mathcomp.analysis.sequences]
_ %:nng (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:nng (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:pos (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:pos (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:nng (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:nng (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:pos (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:pos (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ *? _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ *? _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ +? _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ +? _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ in _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ in _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ in _ | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ in _ | _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ < _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ < _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ < _ | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ < _ | _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ : _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ : _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ : _ | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ : _ | _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ _ _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ _ _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ | _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <= _ < _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <= _ < _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <= _ < _ | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <= _ < _ | _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <- _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <- _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <- _ | _ ) _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\sum_ ( _ <- _ | _ ) _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ \- _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ \- _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ \* _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ \* _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ \+ _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ \+ _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
\- _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
\- _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ *+ _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ *+ _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ ^+ _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ ^+ _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
`| _ | (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
`| _ | (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ * _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ * _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
- _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
- _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ - _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ - _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ + _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ + _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ :> _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ :> _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ < _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ < _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ < _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ < _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ <= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ <= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ <= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ <= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ > _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ > _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ >= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ >= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ < _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ < _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ < _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ < _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ <= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ <= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ <= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ <= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ < _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ <= _ (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
1 (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
1 (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
0 (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
0 (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
-oo (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
-oo (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
+oo (ereal_scope) [notation, in mathcomp.analysis.constructive_ereal]
+oo (ereal_dual_scope) [notation, in mathcomp.analysis.constructive_ereal]
'funpPinj_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'injpPfun_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'pPinj_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'pPbij_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'pinv_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'valLfun_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'valL_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'bijTT_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'bij_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'split_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'surj_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'totalfun_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'funK_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'inj_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'funoK_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'invS_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'invK_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'oinvT_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'oinvP_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'oinvS_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'oinvK_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'mem_fun_ _ (form_scope) [notation, in mathcomp.analysis.functions]
'funS_ _ (form_scope) [notation, in mathcomp.analysis.functions]
[ splitbij of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ bij of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ splitinjfun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ splitinj of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ injfun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ inj of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ splitsurjfun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ splitsurj of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ surjfun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ surj of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ invfun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ inv of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ oinvfun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ oinv of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
[ fun of _ ] (form_scope) [notation, in mathcomp.analysis.functions]
{ fun _ >-> _ } (form_scope) [notation, in mathcomp.analysis.functions]
[ fimfun of _ ] (form_scope) [notation, in mathcomp.analysis.cardinality]
{ fimfun _ >-> _ } (form_scope) [notation, in mathcomp.analysis.cardinality]
[ nnsfun of _ ] (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
{ nnsfun _ >-> _ } (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
[ nnfun of _ ] (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
{ nnfun _ >-> _ } (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
[ sfun of _ ] (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
{ sfun _ >-> _ } (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
[ mfun of _ ] (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
{ mfun _ >-> _ } (form_scope) [notation, in mathcomp.analysis.lebesgue_integral]
$| _ | (form_scope) [notation, in mathcomp.analysis.classical_sets]
[ get _ | _ ] (form_scope) [notation, in mathcomp.analysis.classical_sets]
[ get _ : _ | _ ] (form_scope) [notation, in mathcomp.analysis.classical_sets]
[ get _ | _ ] (form_scope) [notation, in mathcomp.analysis.classical_sets]
_ .`2 (fset_scope) [notation, in mathcomp.analysis.cardinality]
_ .`1 (fset_scope) [notation, in mathcomp.analysis.cardinality]
[ fun _ in _ ] (function_scope) [notation, in mathcomp.analysis.functions]
_ ^-1 (function_scope) [notation, in mathcomp.analysis.functions]
_ ^-1 (function_scope) [notation, in mathcomp.analysis.functions]
_ \_ _ (fun_scope) [notation, in mathcomp.analysis.functions]
_ ^-1 (fun_scope) [notation, in mathcomp.analysis.functions]
_ ^-1 (fun_scope) [notation, in mathcomp.analysis.functions]
@ mine _ (fun_scope) [notation, in mathcomp.analysis.constructive_ereal]
@ maxe _ (fun_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ .-prod (measure_display_scope) [notation, in mathcomp.analysis.measure]
_ ^* (measure_scope) [notation, in mathcomp.analysis.measure]
_ .-cara (measure_display_scope) [notation, in mathcomp.analysis.measure]
_ .-ring (measure_display_scope) [notation, in mathcomp.analysis.measure]
_ .-sigma (measure_display_scope) [notation, in mathcomp.analysis.measure]
_ .-ocitv (measure_display_scope) [notation, in mathcomp.analysis.lebesgue_measure]
{ outer_measure set _ -> \bar _ } (ring_scope) [notation, in mathcomp.analysis.measure]
\d_ _ (ring_scope) [notation, in mathcomp.analysis.measure]
{ measure set _ -> \bar _ } (ring_scope) [notation, in mathcomp.analysis.measure]
{ additive_measure set _ -> \bar _ } (ring_scope) [notation, in mathcomp.analysis.measure]
\esum_ ( _ in _ ) _ (ring_scope) [notation, in mathcomp.analysis.esum]
_ %:nng (ring_scope) [notation, in mathcomp.analysis.signed]
_ %:pos (ring_scope) [notation, in mathcomp.analysis.signed]
_ %:nng (ring_scope) [notation, in mathcomp.analysis.signed]
_ %:pos (ring_scope) [notation, in mathcomp.analysis.signed]
\sum_ ( _ \in _ ) _ (ring_scope) [notation, in mathcomp.analysis.fsbigop]
_ \max _ (ring_scope) [notation, in mathcomp.analysis.mathcomp_extra]
_ \* _ (ring_scope) [notation, in mathcomp.analysis.mathcomp_extra]
\- _ (ring_scope) [notation, in mathcomp.analysis.mathcomp_extra]
\1_ _ (ring_scope) [notation, in mathcomp.analysis.numfun]
_ @`] _ , _ [ (ring_scope) [notation, in mathcomp.analysis.normedtype]
_ @`[ _ , _ ] (ring_scope) [notation, in mathcomp.analysis.normedtype]
-oo (ring_scope) [notation, in mathcomp.analysis.normedtype]
+oo (ring_scope) [notation, in mathcomp.analysis.normedtype]
_ .-sesqui (ring_scope) [notation, in mathcomp.analysis.forms]
'e_ _ (ring_scope) [notation, in mathcomp.analysis.forms]
_ ``_ _ (ring_scope) [notation, in mathcomp.analysis.forms]
[ normed _ ] (ring_scope) [notation, in mathcomp.analysis.sequences]
[ series _ ]_ _ (ring_scope) [notation, in mathcomp.analysis.sequences]
[ sequence _ ]_ _ (ring_scope) [notation, in mathcomp.analysis.sequences]
{ ae _ , _ } (type_scope) [notation, in mathcomp.analysis.measure]
_ .-negligible (type_scope) [notation, in mathcomp.analysis.measure]
{ splitbij _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ bij _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ splitinjfun _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ splitinj _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ injfun _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ inj _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ splitsurjfun _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ splitsurj _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ surjfun _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ surj _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ invfun _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ inv _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ oinvfun _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{ oinv _ >-> _ } (type_scope) [notation, in mathcomp.analysis.functions]
{eclassic _ } (type_scope) [notation, in mathcomp.analysis.boolp]
{classic _ } (type_scope) [notation, in mathcomp.analysis.boolp]
{ distr _ / _ } (type_scope) [notation, in mathcomp.analysis.altreals.distr]
_ .-lipschitz _ (type_scope) [notation, in mathcomp.analysis.normedtype]
_ .-lipschitz_on _ (type_scope) [notation, in mathcomp.analysis.normedtype]
_ .-integrable (type_scope) [notation, in mathcomp.analysis.lebesgue_integral]
_ ^nat (type_scope) [notation, in mathcomp.analysis.sequences]
\near _ & _ , _ (type_scope) [notation, in mathcomp.analysis.topology]
\forall _ & _ \near _ , _ (type_scope) [notation, in mathcomp.analysis.topology]
\forall _ \near _ & _ \near _ , _ (type_scope) [notation, in mathcomp.analysis.topology]
{ near _ & _ , _ } (type_scope) [notation, in mathcomp.analysis.topology]
\near _ , _ (type_scope) [notation, in mathcomp.analysis.topology]
\forall _ \near _ , _ (type_scope) [notation, in mathcomp.analysis.topology]
{ near _ , _ } (type_scope) [notation, in mathcomp.analysis.topology]
{ nonneg \bar _ } (type_scope) [notation, in mathcomp.analysis.constructive_ereal]
{ posnum \bar _ } (type_scope) [notation, in mathcomp.analysis.constructive_ereal]
\bar _ (type_scope) [notation, in mathcomp.analysis.constructive_ereal]
_ %:S [notation, in mathcomp.analysis.altreals.realseq]
_ <=2 _ [notation, in mathcomp.analysis.altreals.realseq]
_ <=1 _ [notation, in mathcomp.analysis.altreals.realseq]
_ .-lipschitz_ _ _ [notation, in mathcomp.analysis.normedtype]
_ =Theta_ _ _ [notation, in mathcomp.analysis.landau]
_ =Omega_ _ _ [notation, in mathcomp.analysis.landau]
_ ~~_ _ _ [notation, in mathcomp.analysis.landau]
_ ~_ _ _ [notation, in mathcomp.analysis.landau]
_ ==O_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ == _ +O_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ =O_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ = _ +O_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ ==O_ _ _ [notation, in mathcomp.analysis.landau]
_ == _ +O_ _ _ [notation, in mathcomp.analysis.landau]
_ =O_ _ _ [notation, in mathcomp.analysis.landau]
_ = _ +O_ _ _ [notation, in mathcomp.analysis.landau]
_ ==o_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ == _ +o_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ =o_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ = _ +o_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
_ ==o_ _ _ [notation, in mathcomp.analysis.landau]
_ == _ +o_ _ _ [notation, in mathcomp.analysis.landau]
_ =o_ _ _ [notation, in mathcomp.analysis.landau]
_ = _ +o_ _ _ [notation, in mathcomp.analysis.landau]
_ ^` ( _ ) [notation, in mathcomp.analysis.derive]
_ ^` () [notation, in mathcomp.analysis.derive]
_ `^ _ [notation, in mathcomp.analysis.exp]
_ ^t _ [notation, in mathcomp.analysis.forms]
_ ^ _ [notation, in mathcomp.analysis.forms]
_ \is_near _ [notation, in mathcomp.analysis.topology]
_ %:E [notation, in mathcomp.analysis.constructive_ereal]
decreasing_seq _ [notation, in mathcomp.analysis.sequences]
increasing_seq _ [notation, in mathcomp.analysis.sequences]
is_diff _ [notation, in mathcomp.analysis.derive]
nondecreasing_seq _ [notation, in mathcomp.analysis.sequences]
nonincreasing_seq _ [notation, in mathcomp.analysis.sequences]
!! _ [notation, in mathcomp.analysis.signed]
'a_O_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
'a_O_ _ _ [notation, in mathcomp.analysis.landau]
'a_o_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
'a_o_ _ _ [notation, in mathcomp.analysis.landau]
'D_ _ _ _ [notation, in mathcomp.analysis.derive]
'D_ _ _ [notation, in mathcomp.analysis.derive]
'd _ _ [notation, in mathcomp.analysis.derive]
'J _ _ [notation, in mathcomp.analysis.derive]
'oinv_ _ [notation, in mathcomp.analysis.functions]
'Omega_ _ _ [notation, in mathcomp.analysis.landau]
'O_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
'O_ _ _ [notation, in mathcomp.analysis.landau]
'O_ _ [notation, in mathcomp.analysis.landau]
'o_( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
'o_ _ _ [notation, in mathcomp.analysis.landau]
'o_ _ [notation, in mathcomp.analysis.landau]
'O [notation, in mathcomp.analysis.landau]
'o [notation, in mathcomp.analysis.landau]
'O _( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
'O '_' _ [notation, in mathcomp.analysis.landau]
'o _( _ \near _ ) _ [notation, in mathcomp.analysis.landau]
'o '_' _ [notation, in mathcomp.analysis.landau]
'Theta_ _ _ [notation, in mathcomp.analysis.landau]
*%E [notation, in mathcomp.analysis.constructive_ereal]
+%dE [notation, in mathcomp.analysis.constructive_ereal]
+%E [notation, in mathcomp.analysis.constructive_ereal]
-%E [notation, in mathcomp.analysis.constructive_ereal]
@ gte _ [notation, in mathcomp.analysis.constructive_ereal]
@ gee _ [notation, in mathcomp.analysis.constructive_ereal]
@ lte _ [notation, in mathcomp.analysis.constructive_ereal]
@ lee _ [notation, in mathcomp.analysis.constructive_ereal]
[bigOmega of _ ] [notation, in mathcomp.analysis.landau]
[bigO of _ ] [notation, in mathcomp.analysis.landau]
[bigO of _ for _ ] [notation, in mathcomp.analysis.landau]
[bigTheta of _ ] [notation, in mathcomp.analysis.landau]
[littleo of _ ] [notation, in mathcomp.analysis.landau]
[littleo of _ for _ ] [notation, in mathcomp.analysis.landau]
[Omega_ _ _ of _ ] [notation, in mathcomp.analysis.landau]
[Omega '_' _ _ of _ ] [notation, in mathcomp.analysis.landau]
[O_( _ \near _ ) _ of _ ] [notation, in mathcomp.analysis.landau]
[O_ _ _ of _ ] [notation, in mathcomp.analysis.landau]
[o_( _ \near _ ) _ of _ ] [notation, in mathcomp.analysis.landau]
[o_ _ _ of _ ] [notation, in mathcomp.analysis.landau]
[O _( _ \near _ ) _ of _ ] [notation, in mathcomp.analysis.landau]
[O '_' _ _ of _ ] [notation, in mathcomp.analysis.landau]
[o '_' _ _ of _ ] [notation, in mathcomp.analysis.landau]
[o _( _ \near _ ) _ of _ ] [notation, in mathcomp.analysis.landau]
[Theta_ _ _ of _ ] [notation, in mathcomp.analysis.landau]
[Theta '_' _ _ of _ ] [notation, in mathcomp.analysis.landau]
[ neq0 of _ ] [notation, in mathcomp.analysis.signed]
[ cmp0 of _ ] [notation, in mathcomp.analysis.signed]
[ le0 of _ ] [notation, in mathcomp.analysis.signed]
[ ge0 of _ ] [notation, in mathcomp.analysis.signed]
[ lt0 of _ ] [notation, in mathcomp.analysis.signed]
[ gt0 of _ ] [notation, in mathcomp.analysis.signed]
[ lipschitz _ | _ in _ ] [notation, in mathcomp.analysis.normedtype]
[ bounded _ | _ in _ ] [notation, in mathcomp.analysis.normedtype]
[ locally _ ] [notation, in mathcomp.analysis.topology]
[ countable of _ ] [notation, in mathcomp.analysis.altreals.discrete]
[ psub _ ] [notation, in mathcomp.analysis.altreals.discrete]
\dlet_ ( _ <- _ ) _ [notation, in mathcomp.analysis.altreals.distr]
\dlim_ ( _ ) _ [notation, in mathcomp.analysis.altreals.distr]
\E_[ _ , _ ] _ [notation, in mathcomp.analysis.altreals.distr]
\E_[ _ ] _ [notation, in mathcomp.analysis.altreals.distr]
\E?_[ _ ] _ [notation, in mathcomp.analysis.altreals.distr]
\P_[ _ , _ ] _ [notation, in mathcomp.analysis.altreals.distr]
\P_[ _ ] _ [notation, in mathcomp.analysis.altreals.distr]
\`| _ | [notation, in mathcomp.analysis.altreals.distr]
\`| _ | [notation, in mathcomp.analysis.altreals.realsum]
`I_ _ [notation, in mathcomp.analysis.classical_sets]
{Omega_ _ _ } [notation, in mathcomp.analysis.landau]
{O_ _ _ } [notation, in mathcomp.analysis.landau]
{o_ _ _ } [notation, in mathcomp.analysis.landau]
{Theta_ _ _ } [notation, in mathcomp.analysis.landau]
{ within _ , continuous _ } [notation, in mathcomp.analysis.topology]
{ family _ , _ -> _ } [notation, in mathcomp.analysis.topology]
{ ptws _ -> _ } [notation, in mathcomp.analysis.topology]
σ:167 [binder, in mathcomp.analysis.altreals.realseq]

Global Index

_

(33778 entries)

Notation Index

A

G

H

J

K

O

Q

V

X

Y

Z

_

(623 entries)

Binder Index

_

(24219 entries)

Module Index

A

G

H

I

J

L

M

O

Q

V

W

X

Y

Z

_

other

(66 entries)

Variable Index

K

Q

V

X

Y

_

other

(1479 entries)

Library Index

A

G

H

I

J

K

O

Q

U

V

W

Y

Z

_

other

(34 entries)

Lemma Index

_

other

(4547 entries)

Constructor Index

A

G

H

J

M

Q

V

Y

Z

_

other

(98 entries)

Axiom Index

A

B

D

E

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Inductive Index

A

G

H

J

Q

R

V

W

Y

Z

_

other

(31 entries)

Projection Index

A

G

H

J

K

O

Q

V

W

X

Y

Z

_

other

(93 entries)

Section Index

K

Q

V

X

Y

_

other

(657 entries)

Instance Index

C

H

J

K

L

M

O

Q

R

V

X

Y

Z

_

other

(73 entries)

Abbreviation Index

J

K

W

Y

Z

_

other

(206 entries)

Definition Index

_

other

(1592 entries)

Record Index

A

G

H

J

K

O

Q

V

W

X

Y

Z

_

other

(55 entries)