mathcomp.ssreflect.tuple

Global Index

_

(78577 entries)

Notation Index

H

J

T

W

X

Y

_

(1807 entries)

Binder Index

_

other

(48032 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(375 entries)

Variable Index

J

W

X

Y

_

other

(3995 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14468 entries)

Constructor Index

J

K

W

Y

_

other

(223 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(133 entries)

Projection Index

D

H

J

K

L

W

X

Y

_

other

(451 entries)

Section Index

J

W

X

Y

_

other

(1387 entries)

Abbreviation Index

Y

_

other

(1144 entries)

Definition Index

Y

_

other

(6179 entries)

Record Index

D

H

J

K

L

W

X

Y

_

other

(247 entries)

O (notation)

\bot [in mathcomp.ssreflect.order]
[ bDistrLatticeType of _ ] (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]
[ bLatticeType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ bLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ bLatticeType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ bLatticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
_ `\` _ (order_scope) [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
~` _ (order_scope) [in mathcomp.ssreflect.order]
\bot [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
[ default_ctbDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
[ distrLatticeType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ distrLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ distrLatticeType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ distrLatticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
><^d%O (fun_scope) [in mathcomp.ssreflect.order]
>=<^d%O (fun_scope) [in mathcomp.ssreflect.order]
<?<=^d%O (fun_scope) [in mathcomp.ssreflect.order]
<?=^d%O (fun_scope) [in mathcomp.ssreflect.order]
>^d%O (fun_scope) [in mathcomp.ssreflect.order]
<^d%O (fun_scope) [in mathcomp.ssreflect.order]
>=^d%O (fun_scope) [in mathcomp.ssreflect.order]
<=^d%O (fun_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 _ (fun_scope) [in mathcomp.ssreflect.order]
@ gcd _ (fun_scope) [in mathcomp.ssreflect.order]
@ sdvd _ (fun_scope) [in mathcomp.ssreflect.order]
@ dvd _ (fun_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]
_ `|` _ (order_scope) [in mathcomp.ssreflect.order]
_ `&` _ (order_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]
><^l%O (fun_scope) [in mathcomp.ssreflect.order]
>=<^l%O (fun_scope) [in mathcomp.ssreflect.order]
<?=^l%O (fun_scope) [in mathcomp.ssreflect.order]
>^l%O (fun_scope) [in mathcomp.ssreflect.order]
<^l%O (fun_scope) [in mathcomp.ssreflect.order]
>=^l%O (fun_scope) [in mathcomp.ssreflect.order]
>=^l%O (fun_scope) [in mathcomp.ssreflect.order]
<=^l%O (fun_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]
_ >< _ (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]
><%O (fun_scope) [in mathcomp.ssreflect.order]
>=<%O (fun_scope) [in mathcomp.ssreflect.order]
<?<=%O (fun_scope) [in mathcomp.ssreflect.order]
<?=%O (fun_scope) [in mathcomp.ssreflect.order]
>%O (fun_scope) [in mathcomp.ssreflect.order]
<%O (fun_scope) [in mathcomp.ssreflect.order]
>=%O (fun_scope) [in mathcomp.ssreflect.order]
<=%O (fun_scope) [in mathcomp.ssreflect.order]
_ \max _ (order_scope) [in mathcomp.ssreflect.order]
_ \min _ (order_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 (fun_scope) [in mathcomp.ssreflect.order]
>=<^p%O (fun_scope) [in mathcomp.ssreflect.order]
<?=^p%O (fun_scope) [in mathcomp.ssreflect.order]
>^p%O (fun_scope) [in mathcomp.ssreflect.order]
<^p%O (fun_scope) [in mathcomp.ssreflect.order]
>=^p%O (fun_scope) [in mathcomp.ssreflect.order]
>=^p%O (fun_scope) [in mathcomp.ssreflect.order]
<=^p%O (fun_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]
[ totalOrderMixin of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
[ porderMixin of _ by <: ] (form_scope) [in mathcomp.ssreflect.order]
\top [in mathcomp.ssreflect.order]
[ tbDistrLatticeType of _ ] (form_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]
[ tbLatticeType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ tbLatticeType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ tbLatticeType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ tbLatticeType of _ for _ ] (form_scope) [in mathcomp.ssreflect.order]
[ orderType of _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ orderType of _ ] (form_scope) [in mathcomp.ssreflect.order]
[ orderType of _ for _ with _ ] (form_scope) [in mathcomp.ssreflect.order]
[ orderType of _ for _ ] (form_scope) [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

_

(78577 entries)

Notation Index

H

J

T

W

X

Y

_

(1807 entries)

Binder Index

_

other

(48032 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(375 entries)

Variable Index

J

W

X

Y

_

other

(3995 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14468 entries)

Constructor Index

J

K

W

Y

_

other

(223 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(133 entries)

Projection Index

D

H

J

K

L

W

X

Y

_

other

(451 entries)

Section Index

J

W

X

Y

_

other

(1387 entries)

Abbreviation Index

Y

_

other

(1144 entries)

Definition Index

Y

_

other

(6179 entries)

Record Index

D

H

J

K

L

W

X

Y

_

other

(247 entries)