mathcomp.ssreflect.tuple

Global Index

_

(76754 entries)

Notation Index

H

J

T

W

X

Y

_

(1892 entries)

Binder Index

_

other

(49588 entries)

Module Index

H

J

K

L

W

X

Y

_

other

(305 entries)

Variable Index

J

W

X

Y

_

other

(4034 entries)

Library Index

K

L

U

W

X

Y

_

other

(94 entries)

Lemma Index

Y

_

other

(14802 entries)

Constructor Index

J

K

W

Y

_

other

(222 entries)

Axiom Index

B

C

D

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(131 entries)

Projection Index

D

H

I

J

K

L

N

O

Q

U

W

X

Y

Z

_

other

(43 entries)

Section Index

J

W

X

Y

_

other

(1392 entries)

Abbreviation Index

Y

_

other

(1140 entries)

Definition Index

Y

_

other

(3066 entries)

Record Index

D

F

H

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(36 entries)

O (notation)

[ bDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
[ bLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ bLatticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
\join_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\bot (order_scope) [in mathcomp.ssreflect.order]
0%O [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
_ `\` _ (order_scope) [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
~` _ (order_scope) [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
[ Order of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ POrder of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
><^d%O (function_scope) [in mathcomp.ssreflect.order]
>=<^d%O (function_scope) [in mathcomp.ssreflect.order]
<?<=^d%O (function_scope) [in mathcomp.ssreflect.order]
<?=^d%O (function_scope) [in mathcomp.ssreflect.order]
>^d%O (function_scope) [in mathcomp.ssreflect.order]
<^d%O (function_scope) [in mathcomp.ssreflect.order]
>=^d%O (function_scope) [in mathcomp.ssreflect.order]
<=^d%O (function_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^d_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^d_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\top^d (order_scope) [in mathcomp.ssreflect.order]
\bot^d (order_scope) [in mathcomp.ssreflect.order]
_ `|^d` _ (order_scope) [in mathcomp.ssreflect.order]
_ `&^d` _ (order_scope) [in mathcomp.ssreflect.order]
_ ><^d _ (order_scope) [in mathcomp.ssreflect.order]
><^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
><^d _ (order_scope) [in mathcomp.ssreflect.order]
_ >=<^d _ (order_scope) [in mathcomp.ssreflect.order]
>=<^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=<^d _ (order_scope) [in mathcomp.ssreflect.order]
_ <^d _ ?<= if _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <^d _ ?<= if _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^d _ ?= iff _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^d _ ?= iff _ (order_scope) [in mathcomp.ssreflect.order]
_ <^d _ <^d _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^d _ <^d _ (order_scope) [in mathcomp.ssreflect.order]
_ <^d _ <=^d _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^d _ <=^d _ (order_scope) [in mathcomp.ssreflect.order]
_ >^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >^d _ (order_scope) [in mathcomp.ssreflect.order]
_ <^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <^d _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^d _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^d _ (order_scope) [in mathcomp.ssreflect.order]
>^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>^d _ (order_scope) [in mathcomp.ssreflect.order]
<^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<^d _ (order_scope) [in mathcomp.ssreflect.order]
>=^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=^d _ (order_scope) [in mathcomp.ssreflect.order]
<=^d _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<=^d _ (order_scope) [in mathcomp.ssreflect.order]
_ ^d (type_scope) [in mathcomp.ssreflect.order]
0^d%O [in mathcomp.ssreflect.order]
1^d%O [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
@ lcm _ (function_scope) [in mathcomp.ssreflect.order]
@ gcd _ (function_scope) [in mathcomp.ssreflect.order]
@ sdvd _ (function_scope) [in mathcomp.ssreflect.order]
@ dvd _ (function_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\lcm_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\gcd_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
_ %<| _ (order_scope) [in mathcomp.ssreflect.order]
_ %| _ (order_scope) [in mathcomp.ssreflect.order]
[ finCDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ finDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ finLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ finPOrderType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ finOrderType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ latticeType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ latticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ latticeType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ latticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
[ lmorphism of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ lmorphism of _ as _ ] (form_scope) [in mathcomp.ssreflect.order]
[ jlmorphism of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ jlmorphism of _ as _ ] (form_scope) [in mathcomp.ssreflect.order]
[ mlmorphism of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ mlmorphism of _ as _ ] (form_scope) [in mathcomp.ssreflect.order]
{ lmorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
{ jlmorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
{ mlmorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
_ `|` _ (order_scope) [in mathcomp.ssreflect.order]
_ `&` _ (order_scope) [in mathcomp.ssreflect.order]
><^l%O (function_scope) [in mathcomp.ssreflect.order]
>=<^l%O (function_scope) [in mathcomp.ssreflect.order]
<?=^l%O (function_scope) [in mathcomp.ssreflect.order]
>^l%O (function_scope) [in mathcomp.ssreflect.order]
<^l%O (function_scope) [in mathcomp.ssreflect.order]
>=^l%O (function_scope) [in mathcomp.ssreflect.order]
>=^l%O (function_scope) [in mathcomp.ssreflect.order]
<=^l%O (function_scope) [in mathcomp.ssreflect.order]
_ `|^l` _ (order_scope) [in mathcomp.ssreflect.order]
_ `&^l` _ (order_scope) [in mathcomp.ssreflect.order]
_ ><^l _ (order_scope) [in mathcomp.ssreflect.order]
><^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
><^l _ (order_scope) [in mathcomp.ssreflect.order]
_ >=<^l _ (order_scope) [in mathcomp.ssreflect.order]
>=<^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=<^l _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^l _ ?= iff _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^l _ ?= iff _ (order_scope) [in mathcomp.ssreflect.order]
_ <^l _ <^l _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^l _ <^l _ (order_scope) [in mathcomp.ssreflect.order]
_ <^l _ <=^l _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^l _ <=^l _ (order_scope) [in mathcomp.ssreflect.order]
_ >^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >^l _ (order_scope) [in mathcomp.ssreflect.order]
_ <^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <^l _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^l _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^l _ (order_scope) [in mathcomp.ssreflect.order]
>^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>^l _ (order_scope) [in mathcomp.ssreflect.order]
<^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<^l _ (order_scope) [in mathcomp.ssreflect.order]
>=^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=^l _ (order_scope) [in mathcomp.ssreflect.order]
<=^l _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<=^l _ (order_scope) [in mathcomp.ssreflect.order]
{ omorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
_ >< _ (order_scope) [in mathcomp.ssreflect.order]
_ >=< _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ (order_scope) [in mathcomp.ssreflect.order]
[ porderType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ porderType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ porderType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ porderType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
_ \max _ (function_scope) [in mathcomp.ssreflect.order]
_ \min _ (function_scope) [in mathcomp.ssreflect.order]
><%O (function_scope) [in mathcomp.ssreflect.order]
>=<%O (function_scope) [in mathcomp.ssreflect.order]
<?<=%O (function_scope) [in mathcomp.ssreflect.order]
<?=%O (function_scope) [in mathcomp.ssreflect.order]
>%O (function_scope) [in mathcomp.ssreflect.order]
<%O (function_scope) [in mathcomp.ssreflect.order]
>=%O (function_scope) [in mathcomp.ssreflect.order]
<=%O (function_scope) [in mathcomp.ssreflect.order]
[ arg max_ ( _ > _ ) _ ] (order_scope) [in mathcomp.ssreflect.order]
[ arg max_ ( _ > _ in _ ) _ ] (order_scope) [in mathcomp.ssreflect.order]
[ arg max_ ( _ > _ | _ ) _ ] (order_scope) [in mathcomp.ssreflect.order]
[ arg min_ ( _ < _ ) _ ] (order_scope) [in mathcomp.ssreflect.order]
[ arg min_ ( _ < _ in _ ) _ ] (order_scope) [in mathcomp.ssreflect.order]
[ arg min_ ( _ < _ | _ ) _ ] (order_scope) [in mathcomp.ssreflect.order]
_ >< _ (order_scope) [in mathcomp.ssreflect.order]
>< _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>< _ (order_scope) [in mathcomp.ssreflect.order]
_ >=< _ (order_scope) [in mathcomp.ssreflect.order]
>=< _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=< _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ ?<= if _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ ?<= if _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ ?= iff _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ ?= iff _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ < _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ < _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ <= _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ <= _ (order_scope) [in mathcomp.ssreflect.order]
_ > _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ > _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ < _ (order_scope) [in mathcomp.ssreflect.order]
_ >= _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >= _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <= _ (order_scope) [in mathcomp.ssreflect.order]
> _ :> _ (order_scope) [in mathcomp.ssreflect.order]
> _ (order_scope) [in mathcomp.ssreflect.order]
< _ :> _ (order_scope) [in mathcomp.ssreflect.order]
< _ (order_scope) [in mathcomp.ssreflect.order]
>= _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>= _ (order_scope) [in mathcomp.ssreflect.order]
<= _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<= _ (order_scope) [in mathcomp.ssreflect.order]
_ *l _ (type_scope) [in mathcomp.ssreflect.order]
_ *lexi[ _ ] _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ *p _ (type_scope) [in mathcomp.ssreflect.order]
_ *prod[ _ ] _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
><^p%O (function_scope) [in mathcomp.ssreflect.order]
>=<^p%O (function_scope) [in mathcomp.ssreflect.order]
<?=^p%O (function_scope) [in mathcomp.ssreflect.order]
>^p%O (function_scope) [in mathcomp.ssreflect.order]
<^p%O (function_scope) [in mathcomp.ssreflect.order]
>=^p%O (function_scope) [in mathcomp.ssreflect.order]
>=^p%O (function_scope) [in mathcomp.ssreflect.order]
<=^p%O (function_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^p_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^p_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
_ `|^p` _ (order_scope) [in mathcomp.ssreflect.order]
_ `&^p` _ (order_scope) [in mathcomp.ssreflect.order]
_ ><^p _ (order_scope) [in mathcomp.ssreflect.order]
><^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
><^p _ (order_scope) [in mathcomp.ssreflect.order]
_ >=<^p _ (order_scope) [in mathcomp.ssreflect.order]
>=<^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=<^p _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^p _ ?= iff _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^p _ ?= iff _ (order_scope) [in mathcomp.ssreflect.order]
_ <^p _ <^p _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^p _ <^p _ (order_scope) [in mathcomp.ssreflect.order]
_ <^p _ <=^p _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^p _ <=^p _ (order_scope) [in mathcomp.ssreflect.order]
_ >^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >^p _ (order_scope) [in mathcomp.ssreflect.order]
_ <^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <^p _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^p _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^p _ (order_scope) [in mathcomp.ssreflect.order]
>^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>^p _ (order_scope) [in mathcomp.ssreflect.order]
<^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<^p _ (order_scope) [in mathcomp.ssreflect.order]
>=^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=^p _ (order_scope) [in mathcomp.ssreflect.order]
<=^p _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<=^p _ (order_scope) [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
{ subset _ } (type_scope) [in mathcomp.ssreflect.order]
{ subset [ _ ] _ } (type_scope) [in mathcomp.ssreflect.order]
{ subset _ } [in mathcomp.ssreflect.order]
[ SubChoice_isSubOrder of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isSubOrder of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isSubOrder of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isSubOrder of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubLattice_isSubOrder of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubLattice_isSubOrder of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isTBSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isTBSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isTBSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isTBSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isTSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isTSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isTSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isTSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isBSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isBSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isBSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isBSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isSubLattice of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubPOrder_isSubLattice of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isSubPOrder of _ by <: with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ SubChoice_isSubPOrder of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ tbDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
{ tblmorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
{ tlmorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
{ blmorphism _ -> _ } (type_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\top (order_scope) [in mathcomp.ssreflect.order]
1%O [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
_ .-tuplelexi (type_scope) [in mathcomp.ssreflect.order]
_ .-tuplelexi[ _ ] (type_scope) [in mathcomp.ssreflect.order]
_ .-tuple (type_scope) [in mathcomp.ssreflect.order]
_ .-tupleprod (type_scope) [in mathcomp.ssreflect.order]
_ .-tupleprod[ _ ] (type_scope) [in mathcomp.ssreflect.order]
_ .-tuple (type_scope) [in mathcomp.ssreflect.order]

Global Index

_

(76754 entries)

Notation Index

H

J

T

W

X

Y

_

(1892 entries)

Binder Index

_

other

(49588 entries)

Module Index

H

J

K

L

W

X

Y

_

other

(305 entries)

Variable Index

J

W

X

Y

_

other

(4034 entries)

Library Index

K

L

U

W

X

Y

_

other

(94 entries)

Lemma Index

Y

_

other

(14802 entries)

Constructor Index

J

K

W

Y

_

other

(222 entries)

Axiom Index

B

C

D

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(131 entries)

Projection Index

D

H

I

J

K

L

N

O

Q

U

W

X

Y

Z

_

other

(43 entries)

Section Index

J

W

X

Y

_

other

(1392 entries)

Abbreviation Index

Y

_

other

(1140 entries)

Definition Index

Y

_

other

(3066 entries)

Record Index

D

F

H

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(36 entries)