Top source

Notations

Files

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Definitions

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Lemmas

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Abbreviations

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Notations

no scope

'D_ x x [not, in mathcomp.analysis.derive] (no scope)
'D_ x x [not, in mathcomp.analysis.derive] (no scope)
'D_ x x x [not, in mathcomp.analysis.derive] (no scope)
'D_ x x x [not, in mathcomp.analysis.derive] (no scope)
'J x x [not, in mathcomp.analysis.derive] (no scope)
'M_ x x [not, in mathcomp.analysis.probability_theory.random_variable] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'O [not, in mathcomp.analysis.landau] (no scope)
'O '_' x [not, in mathcomp.analysis.landau] (no scope)
'O '_' x [not, in mathcomp.analysis.landau] (no scope)
'O _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'O _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'O_ x [not, in mathcomp.analysis.landau] (no scope)
'O_ x x [not, in mathcomp.analysis.landau] (no scope)
'O_ x x [not, in mathcomp.analysis.landau] (no scope)
'O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
'Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
'Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
'Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
'V_ x [ x ] [not, in mathcomp.analysis.probability_theory.random_variable] (no scope)
'V_ x [ x ] [not, in mathcomp.analysis.probability_theory.random_variable] (no scope)
'a_O_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_O_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'a_O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'a_o_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_o_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'a_o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'd x '/d x [not, in mathcomp.analysis.lebesgue_integral_theory.radon_nikodym] (no scope)
'd x '/d x [not, in mathcomp.analysis.lebesgue_integral_theory.radon_nikodym] (no scope)
'd x x [not, in mathcomp.analysis.derive] (no scope)
'd x x [not, in mathcomp.analysis.derive] (no scope)
'd x x [not, in mathcomp.analysis.derive] (no scope)
'd1 x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under] (no scope)
'd1 x [not, in mathcomp.analysis.gauss_integral] (no scope)
'o [not, in mathcomp.analysis.landau] (no scope)
'o '_' x [not, in mathcomp.analysis.landau] (no scope)
'o '_' x [not, in mathcomp.analysis.landau] (no scope)
'o _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'o _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'o_ x [not, in mathcomp.analysis.landau] (no scope)
'o_ x x [not, in mathcomp.analysis.landau] (no scope)
'o_ x x [not, in mathcomp.analysis.landau] (no scope)
'o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'oinv_ x [not, in mathcomp.classical.functions] (no scope)
*%E [not, in mathcomp.reals.constructive_ereal] (no scope)
*%M [not, in mathcomp.experimental_reals.xfinmap] (no scope)
+%E [not, in mathcomp.reals.constructive_ereal] (no scope)
+%E [not, in mathcomp.reals.constructive_ereal] (no scope)
+%E [not, in mathcomp.reals.constructive_ereal] (no scope)
+%dE [not, in mathcomp.reals.constructive_ereal] (no scope)
+%dE [not, in mathcomp.reals.constructive_ereal] (no scope)
+%dE [not, in mathcomp.reals.constructive_ereal] (no scope)
+oo [not, in mathcomp.analysis.normedtype_theory.normed_module] (no scope)
+oo [not, in mathcomp.analysis.landau] (no scope)
-%E [not, in mathcomp.reals.constructive_ereal] (no scope)
1 [not, in mathcomp.experimental_reals.xfinmap] (no scope)
@ gee x [not, in mathcomp.reals.constructive_ereal] (no scope)
@ gte x [not, in mathcomp.reals.constructive_ereal] (no scope)
@ lee x [not, in mathcomp.reals.constructive_ereal] (no scope)
@ lte x [not, in mathcomp.reals.constructive_ereal] (no scope)
[ bounded x | x in x ] [not, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule] (no scope)
[ locally x ] [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
[ locally x ] [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
[ psub x ] [not, in mathcomp.experimental_reals.discrete] (no scope)
[O '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[bigOmega of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigOmega of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigOmega of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[bigTheta of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigTheta of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigTheta of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
\E?_[ x ] x [not, in mathcomp.experimental_reals.distr] (no scope)
\E_[ x , x ] x [not, in mathcomp.experimental_reals.distr] (no scope)
\E_[ x ] x [not, in mathcomp.experimental_reals.distr] (no scope)
\P_[ x , x ] x [not, in mathcomp.experimental_reals.distr] (no scope)
\P_[ x ] x [not, in mathcomp.experimental_reals.distr] (no scope)
\`| x | [not, in mathcomp.experimental_reals.realsum] (no scope)
\`| x | [not, in mathcomp.experimental_reals.distr] (no scope)
\dlet_ ( x <- x ) x [not, in mathcomp.experimental_reals.distr] (no scope)
\dlet_ ( x <- x ) x [not, in mathcomp.experimental_reals.distr] (no scope)
\dlim_ ( x ) x [not, in mathcomp.experimental_reals.distr] (no scope)
\dlim_ ( x ) x [not, in mathcomp.experimental_reals.distr] (no scope)
\esum_ ( x in x ) x [not, in mathcomp.analysis.esum] (no scope)
\esum_ ( x in x ) x [not, in mathcomp.analysis.esum] (no scope)
\esum_ ( x in x ) x [not, in mathcomp.analysis.esum] (no scope)
\int_ ( x in x ) x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition] (no scope)
`I_ x [not, in mathcomp.classical.classical_sets] (no scope)
decreasing_fun x [not, in mathcomp.classical.unstable] (no scope)
decreasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
increasing_fun x [not, in mathcomp.classical.unstable] (no scope)
increasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
is_diff x [not, in mathcomp.analysis.derive] (no scope)
mu^* [not, in mathcomp.analysis.measure_theory.measure_extension] (no scope)
nondecreasing_fun x [not, in mathcomp.classical.unstable] (no scope)
nondecreasing_seq x [not, in mathcomp.classical.unstable] (no scope)
nondecreasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
nonincreasing_fun x [not, in mathcomp.classical.unstable] (no scope)
nonincreasing_seq x [not, in mathcomp.classical.unstable] (no scope)
nonincreasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
weak_open x [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ all1 x } [not, in mathcomp.classical.filter] (no scope)
{ all2 x } [not, in mathcomp.classical.filter] (no scope)
{ all3 x } [not, in mathcomp.classical.filter] (no scope)
{ allA x } [not, in mathcomp.classical.wochoice] (no scope)
{ compact-open , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ compact-open , x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ family x , x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{O_ x x } [not, in mathcomp.analysis.landau] (no scope)
{O_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Omega_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Omega_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Theta_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Theta_ x x } [not, in mathcomp.analysis.landau] (no scope)
{o_ x x } [not, in mathcomp.analysis.landau] (no scope)
{o_ x x } [not, in mathcomp.analysis.landau] (no scope)
{o_ x x } [not, in mathcomp.analysis.landau] (no scope)
x %:E [not, in mathcomp.reals.constructive_ereal] (no scope)
x %:S [not, in mathcomp.experimental_reals.realseq] (no scope)
x * x [not, in mathcomp.experimental_reals.xfinmap] (no scope)
x *? x [not, in mathcomp.reals.constructive_ereal] (no scope)
x *` x [not, in mathcomp.analysis.normedtype_theory.vitali_lemma] (no scope)
x +? x [not, in mathcomp.reals.constructive_ereal] (no scope)
x .-fker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-ftker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-ker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-negligible [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x .-null_set [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x .-pker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-ring [not, in mathcomp.analysis.measure_theory.measure_function] (no scope)
x .-ring.-measurable [not, in mathcomp.analysis.measure_theory.measure_function] (no scope)
x .-sfker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-sigmafker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-spker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x < x [not, in mathcomp.classical.boolp] (no scope)
x <= x [not, in mathcomp.classical.boolp] (no scope)
x <=1 x [not, in mathcomp.experimental_reals.realseq] (no scope)
x <=2 x [not, in mathcomp.experimental_reals.realseq] (no scope)
x <| x |> x [not, in mathcomp.analysis.convex] (no scope)
x = x %[ae x ] [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x = x %[ae x in x ] [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x = x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==O_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==O_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==o_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==o_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =O_ x x [not, in mathcomp.analysis.landau] (no scope)
x =O_ x x [not, in mathcomp.analysis.landau] (no scope)
x =O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
x =Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
x =Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
x =Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
x =o_ x x [not, in mathcomp.analysis.landau] (no scope)
x =o_ x x [not, in mathcomp.analysis.landau] (no scope)
x =o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x >>= x [not, in mathcomp.analysis.lebesgue_integral_theory.giry] (no scope)
x \is_near x [not, in mathcomp.classical.filter] (no scope)
x ^* [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation] (no scope)
x ^* [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation] (no scope)
x ^` ( x ) [not, in mathcomp.analysis.derive] (no scope)
x ^` () [not, in mathcomp.analysis.derive] (no scope)
x ^° [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
x `<< x [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x `<=` x [not, in mathcomp.classical.classical_sets] (no scope)
x `^ x [not, in mathcomp.analysis.exp] (no scope)
x `^ x [not, in mathcomp.analysis.exp] (no scope)
x ~_ x x [not, in mathcomp.analysis.landau] (no scope)
x ~~_ x x [not, in mathcomp.analysis.landau] (no scope)
x ° [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
x ≡μ x [not, in mathcomp.analysis.lebesgue_integral_theory.giry] (no scope)

big_scope

\big [ x / x ]_ ( x <= x <oo ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x <= x <oo | x ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x <oo ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x <oo | x ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x \in x ) x [not, in mathcomp.classical.fsbigop] (in big_scope)
\big [ x / x ]_ ( x \in x ) x [not, in mathcomp.classical.fsbigop] (in big_scope)

bool_scope

`[< x >] [not, in mathcomp.classical.boolp] (in bool_scope)

card_scope

x #!= x [not, in mathcomp.classical.cardinality] (in card_scope)
x #<= x [not, in mathcomp.classical.cardinality] (in card_scope)
x #= x [not, in mathcomp.classical.cardinality] (in card_scope)
x #>= x [not, in mathcomp.classical.cardinality] (in card_scope)

charge_scope

'd x '/d x [not, in mathcomp.analysis.lebesgue_integral_theory.radon_nikodym] (in charge_scope)
x .-negative_set [not, in mathcomp.analysis.measure_theory.signed_measure] (in charge_scope)
x .-positive_set [not, in mathcomp.analysis.measure_theory.signed_measure] (in charge_scope)

classical_set_scope

'measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<M x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<d x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<l x , x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<l x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<r x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<s x , x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<s x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<sr x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
[ cvg x in x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
[ disjoint x & x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ lim x in x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
[ set : x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set ~ x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x : x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x : x | x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x ; x ; .. ; x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x | x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x | x in x & x in x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x | x in x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set` x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x : x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x < x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x >= x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x in x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ x x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x : x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x < x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x >= x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x in x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ x x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\oo [not, in mathcomp.classical.filter] (in classical_set_scope)
`[ x , +oo [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`[ x , x [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`[ x , x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] -oo , +oo [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] -oo , x [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] -oo , x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] x , +oo [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] x , x [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] x , x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
{ ptws , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in classical_set_scope)
{ uniform , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in classical_set_scope)
{ uniform x , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in classical_set_scope)
{ within x , continuous x } [not, in mathcomp.analysis.topology_theory.subspace_topology] (in classical_set_scope)
~` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x !=set0 [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x *` x [not, in mathcomp.analysis.normedtype_theory.vitali_lemma] (in classical_set_scope)
x --> x [not, in mathcomp.classical.filter] (in classical_set_scope)
x .-cara.-measurable [not, in mathcomp.analysis.measure_theory.measure_extension] (in classical_set_scope)
x .-caratheodory [not, in mathcomp.analysis.measure_theory.measure_extension] (in classical_set_scope)
x .-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .-ocitv.-measurable [not, in mathcomp.analysis.lebesgue_stieltjes_measure] (in classical_set_scope)
x .-open.-measurable [not, in mathcomp.analysis.lebesgue_stieltjes_measure] (in classical_set_scope)
x .-preimage.-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .-prod.-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .-ring.-measurable [not, in mathcomp.analysis.measure_theory.measure_function] (in classical_set_scope)
x .-sigma.-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .`1 [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x .`2 [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x @ x [not, in mathcomp.classical.filter] (in classical_set_scope)
x @[ x --> x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
x @[ x \oo ] [not, in mathcomp.classical.filter] (in classical_set_scope)
x @^-1` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x @` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x @`[ x , x ] [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in classical_set_scope)
x @`] x , x [ [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in classical_set_scope)
x ^' [not, in mathcomp.analysis.topology_theory.topology_structure] (in classical_set_scope)
x ^'+ [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^'+ [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^'- [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^'- [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^` ( x ) [not, in mathcomp.analysis.derive] (in classical_set_scope)
x ^` () [not, in mathcomp.analysis.derive] (in classical_set_scope)
x `#` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `&` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `*` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `*`` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `+` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `<=>` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `<=` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `<` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `=>` x [not, in mathcomp.classical.filter] (in classical_set_scope)
x `@ x [not, in mathcomp.classical.filter] (in classical_set_scope)
x `@[ x --> x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
x `\ x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `\` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x ``*` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `x` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `|` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x |` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x ° [not, in mathcomp.analysis.topology_theory.topology_structure] (in classical_set_scope)

convex_scope

x <| x |> x [not, in mathcomp.analysis.convex] (in convex_scope)

ereal_dual_scope

+oo [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
- 1 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
-oo [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
0 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
1 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x : x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <- x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x \in x ) x [not, in mathcomp.analysis.ereal] (in ereal_dual_scope)
\sum_ ( x in x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ x x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
`| x | [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:E [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:dE [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x * x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x *+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x *? x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x +? x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x / x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x > x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x >= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \* x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x ^+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x ^-1 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)

ereal_scope

'E_ x [ x ] [not, in mathcomp.analysis.probability_theory.random_variable] (in ereal_scope)
'N[ x ]_ x [ x ] [not, in mathcomp.analysis.hoelder] (in ereal_scope)
+oo [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
- 1 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
-oo [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
0 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
1 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
[ sequence x ]_ x [not, in mathcomp.analysis.sequences] (in ereal_scope)
[ series x ]_ x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\int [ x ]_ ( x in x ) x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition] (in ereal_scope)
\int [ x ]_ x x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition] (in ereal_scope)
\prod_ ( x : x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x : x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <- x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <- x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <= x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <= x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x in x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x in x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ x x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x : x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <- x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <= x <oo ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x <= x <oo | x ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x <oo ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x <oo | x ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x \in x ) x [not, in mathcomp.analysis.ereal] (in ereal_scope)
\sum_ ( x in x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ x x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
`| x | [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x * x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x *+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x *? x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x *^-1? x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x +? x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x / x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x :> x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x :> x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x > x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x >= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \* x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \; x [not, in mathcomp.analysis.kernel] (in ereal_scope)
x \x x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini] (in ereal_scope)
x \x^ x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini] (in ereal_scope)
x ^* [not, in mathcomp.analysis.hoelder] (in ereal_scope)
x ^+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x ^-1 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x ^\+ [not, in mathcomp.analysis.numfun] (in ereal_scope)
x ^\- [not, in mathcomp.analysis.numfun] (in ereal_scope)
x `^ x [not, in mathcomp.analysis.exp] (in ereal_scope)
x `^? ( x +? x ) [not, in mathcomp.analysis.exp] (in ereal_scope)

form_scope

$| x | [not, in mathcomp.classical.classical_sets] (in form_scope)
'bijTT_ x [not, in mathcomp.classical.functions] (in form_scope)
'bij_ x [not, in mathcomp.classical.functions] (in form_scope)
'funK_ x [not, in mathcomp.classical.functions] (in form_scope)
'funS_ x [not, in mathcomp.classical.functions] (in form_scope)
'funoK_ x [not, in mathcomp.classical.functions] (in form_scope)
'funpPinj_ x [not, in mathcomp.classical.functions] (in form_scope)
'inj_ x [not, in mathcomp.classical.functions] (in form_scope)
'injpPfun_ x [not, in mathcomp.classical.functions] (in form_scope)
'invK_ x [not, in mathcomp.classical.functions] (in form_scope)
'invS_ x [not, in mathcomp.classical.functions] (in form_scope)
'mem_fun_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvK_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvP_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvS_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvT_ x [not, in mathcomp.classical.functions] (in form_scope)
'pPbij_ x [not, in mathcomp.classical.functions] (in form_scope)
'pPinj_ x [not, in mathcomp.classical.functions] (in form_scope)
'pinv_ x [not, in mathcomp.classical.functions] (in form_scope)
'split_ x [not, in mathcomp.classical.functions] (in form_scope)
'surj_ x [not, in mathcomp.classical.functions] (in form_scope)
'totalfun_ x [not, in mathcomp.classical.functions] (in form_scope)
'valL_ x [not, in mathcomp.classical.functions] (in form_scope)
'valLfun_ x [not, in mathcomp.classical.functions] (in form_scope)
[ SubChoice_isSubComPzRing of x by <: ] [not, in mathcomp.analysis.measurable_realfun] (in form_scope)
[ SubPzRing_isSubComPzRing of x by <: ] [not, in mathcomp.analysis.numfun] (in form_scope)
[ bij of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ fimfun of x ] [not, in mathcomp.classical.cardinality] (in form_scope)
[ fun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ get x : x | x ] [not, in mathcomp.classical.classical_sets] (in form_scope)
[ get x | x ] [not, in mathcomp.classical.classical_sets] (in form_scope)
[ get x | x ] [not, in mathcomp.classical.classical_sets] (in form_scope)
[ inj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ injfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ inv of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ invfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ mfun of x ] [not, in mathcomp.analysis.measure_theory.measurable_function] (in form_scope)
[ nnfun of x ] [not, in mathcomp.analysis.numfun] (in form_scope)
[ nnsfun of x ] [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)
[ oinv of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ oinvfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ sfun of x ] [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)
[ splitbij of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitinj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitinjfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitsurj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitsurjfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ surj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ surjfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
{ RV x >-> x } [not, in mathcomp.analysis.probability_theory.random_variable] (in form_scope)
{ dRV x >-> x } [not, in mathcomp.analysis.probability_theory.random_variable] (in form_scope)
{ dmfun x >-> x } [not, in mathcomp.analysis.probability_theory.random_variable] (in form_scope)
{ fimfun x >-> x } [not, in mathcomp.classical.cardinality] (in form_scope)
{ fun x >-> x } [not, in mathcomp.classical.functions] (in form_scope)
{ mfun x >-> x } [not, in mathcomp.analysis.measure_theory.measurable_function] (in form_scope)
{ mfun_ x , x >-> x } [not, in mathcomp.analysis.hoelder] (in form_scope)
{ nnfun x >-> x } [not, in mathcomp.analysis.numfun] (in form_scope)
{ nnsfun x >-> x } [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)
{ sfun x >-> x } [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)

fset_scope

x .`1 [not, in mathcomp.classical.cardinality] (in fset_scope)
x .`2 [not, in mathcomp.classical.cardinality] (in fset_scope)

function_scope

@ maxe x [not, in mathcomp.reals.constructive_ereal] (in function_scope)
@ mine x [not, in mathcomp.reals.constructive_ereal] (in function_scope)
[ fun x in x ] [not, in mathcomp.classical.functions] (in function_scope)
x \_ x [not, in mathcomp.classical.functions] (in function_scope)
x ^-1 [not, in mathcomp.classical.functions] (in function_scope)
x ^-1 [not, in mathcomp.classical.functions] (in function_scope)

measure_display_scope

x .-cara [not, in mathcomp.analysis.measure_theory.measure_extension] (in measure_display_scope)
x .-ocitv [not, in mathcomp.analysis.lebesgue_stieltjes_measure] (in measure_display_scope)
x .-open [not, in mathcomp.analysis.lebesgue_stieltjes_measure] (in measure_display_scope)
x .-preimage [not, in mathcomp.analysis.measure_theory.measurable_structure] (in measure_display_scope)
x .-prod [not, in mathcomp.analysis.measure_theory.measurable_structure] (in measure_display_scope)
x .-ring [not, in mathcomp.analysis.measure_theory.measure_function] (in measure_display_scope)
x .-sigma [not, in mathcomp.analysis.measure_theory.measurable_structure] (in measure_display_scope)

measure_scope

x ^* [not, in mathcomp.analysis.measure_theory.measure_extension] (in measure_scope)

relation_scope

x \; x [not, in mathcomp.classical.classical_sets] (in relation_scope)
x ^-1 [not, in mathcomp.classical.classical_sets] (in relation_scope)

ring_scope

+oo [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
+oo_ x [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
-oo [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
-oo_ x [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
[ normed x ] [not, in mathcomp.analysis.sequences] (in ring_scope)
[ sequence x ]_ x [not, in mathcomp.analysis.sequences] (in ring_scope)
[ series x ]_ x [not, in mathcomp.analysis.sequences] (in ring_scope)
\1_ x [not, in mathcomp.analysis.numfun] (in ring_scope)
\d_ x [not, in mathcomp.analysis.measure_theory.dirac_measure] (in ring_scope)
\esum_ ( x in x ) x [not, in mathcomp.analysis.esum] (in ring_scope)
\int [ x ]_ ( x in x ) x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral] (in ring_scope)
\int [ x ]_ x x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral] (in ring_scope)
\sum_ ( x \in x ) x [not, in mathcomp.classical.fsbigop] (in ring_scope)
`1- x [not, in mathcomp.classical.unstable] (in ring_scope)
{ additive_charge set x -> \bar x } [not, in mathcomp.analysis.measure_theory.signed_measure] (in ring_scope)
{ charge set x -> \bar x } [not, in mathcomp.analysis.measure_theory.signed_measure] (in ring_scope)
{ content set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ finite_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ outer_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_extension] (in ring_scope)
{ sfinite_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ sigma_finite_content set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ sigma_finite_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
x .~ [not, in mathcomp.classical.unstable] (in ring_scope)
x @`[ x , x ] [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
x @`] x , x [ [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
x \^-1 [not, in mathcomp.classical.unstable] (in ring_scope)
x ^\+ [not, in mathcomp.analysis.numfun] (in ring_scope)
x ^\- [not, in mathcomp.analysis.numfun] (in ring_scope)
x `^ x [not, in mathcomp.analysis.exp] (in ring_scope)

signature_scope

x ++> x [not, in mathcomp.classical.unstable] (in signature_scope)
x ==> x [not, in mathcomp.classical.unstable] (in signature_scope)
x ~~> x [not, in mathcomp.classical.unstable] (in signature_scope)

type_scope

[ lipschitz x | x in x ] [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
\Forall x .. x , x [not, in mathcomp.classical.contra] (in type_scope)
\bar ^d x [not, in mathcomp.reals.constructive_ereal] (in type_scope)
\bar x [not, in mathcomp.reals.constructive_ereal] (in type_scope)
\forall x & x \near x , x [not, in mathcomp.classical.filter] (in type_scope)
\forall x \ae x , x [not, in mathcomp.analysis.measure_theory.measure_negligible] (in type_scope)
\forall x \near x & x \near x , x [not, in mathcomp.classical.filter] (in type_scope)
\forall x \near x , x [not, in mathcomp.classical.filter] (in type_scope)
\near x & x , x [not, in mathcomp.classical.filter] (in type_scope)
\near x , x [not, in mathcomp.classical.filter] (in type_scope)
{ ae x , x } [not, in mathcomp.analysis.measure_theory.measure_negligible] (in type_scope)
{ bij x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ distr x / x } [not, in mathcomp.experimental_reals.distr] (in type_scope)
{ family x , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ in <= x , x } [not, in mathcomp.classical.wochoice] (in type_scope)
{ inj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ injfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ inv x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ invfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ linear_continuous x -> x | x } [not, in mathcomp.analysis.normedtype_theory.tvs] (in type_scope)
{ linear_continuous x -> x } [not, in mathcomp.analysis.normedtype_theory.tvs] (in type_scope)
{ near x & x , x } [not, in mathcomp.classical.filter] (in type_scope)
{ near x , x } [not, in mathcomp.classical.filter] (in type_scope)
{ nonneg \bar x } [not, in mathcomp.reals.constructive_ereal] (in type_scope)
{ oinv x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ oinvfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ path x from x to x in x } [not, in mathcomp.analysis.homotopy_theory.continuous_path] (in type_scope)
{ path x from x to x } [not, in mathcomp.analysis.homotopy_theory.continuous_path] (in type_scope)
{ posnum \bar x } [not, in mathcomp.reals.constructive_ereal] (in type_scope)
{ ptws x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ splitbij x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitinj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitinjfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitsurj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitsurjfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ surj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ surjfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ uniform x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ uniform` x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{classic x } [not, in mathcomp.classical.boolp] (in type_scope)
{eclassic x } [not, in mathcomp.classical.boolp] (in type_scope)
x .-Lspace x [not, in mathcomp.analysis.hoelder] (in type_scope)
x .-integrable [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable] (in type_scope)
x .-lipschitz x [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
x .-lipschitz_ x x [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
x .-lipschitz_on x [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
x .-negligible [not, in mathcomp.analysis.measure_theory.measure_negligible] (in type_scope)
x <<=> x [not, in mathcomp.classical.functions] (in type_scope)
x <<~ x [not, in mathcomp.classical.functions] (in type_scope)
x <<~> x [not, in mathcomp.classical.functions] (in type_scope)
x <=> x [not, in mathcomp.classical.functions] (in type_scope)
x <~ x [not, in mathcomp.classical.functions] (in type_scope)
x <~> x [not, in mathcomp.classical.functions] (in type_scope)
x ==>> x [not, in mathcomp.classical.functions] (in type_scope)
x =>> x [not, in mathcomp.classical.functions] (in type_scope)
x >=> x [not, in mathcomp.classical.functions] (in type_scope)
x >>=> x [not, in mathcomp.classical.functions] (in type_scope)
x >>~> x [not, in mathcomp.classical.functions] (in type_scope)
x >~> x [not, in mathcomp.classical.functions] (in type_scope)
x ^nat [not, in mathcomp.classical.classical_sets] (in type_scope)
x ^nat [not, in mathcomp.analysis.sequences] (in type_scope)
x ~> x [not, in mathcomp.classical.functions] (in type_scope)
x ~>> x [not, in mathcomp.classical.functions] (in type_scope)
x ~~>> x [not, in mathcomp.classical.functions] (in type_scope)