mathcomp.ssreflect.tuple

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)

O (notation)

\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]
_ `\` _ (order_scope) [in mathcomp.ssreflect.order]
~` _ (order_scope) [in mathcomp.ssreflect.order]
_ .-tuplelexi [in mathcomp.ssreflect.order]
_ .-tupleprod [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]
\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]
[ 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]
_ \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]
\top (order_scope) [in mathcomp.ssreflect.order]
\bot (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]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_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]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (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]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (type_scope) [in mathcomp.ssreflect.order]
_ * _ (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]
><^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]
><^sp%O (function_scope) [in mathcomp.ssreflect.order]
>=<^sp%O (function_scope) [in mathcomp.ssreflect.order]
<?=^sp%O (function_scope) [in mathcomp.ssreflect.order]
>^sp%O (function_scope) [in mathcomp.ssreflect.order]
<^sp%O (function_scope) [in mathcomp.ssreflect.order]
>=^sp%O (function_scope) [in mathcomp.ssreflect.order]
>=^sp%O (function_scope) [in mathcomp.ssreflect.order]
<=^sp%O (function_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\meet^sp_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ in _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ in _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ <= _ < _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ <= _ < _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ : _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ : _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ _ _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ <- _ ) _ (order_scope) [in mathcomp.ssreflect.order]
\join^sp_ ( _ <- _ | _ ) _ (order_scope) [in mathcomp.ssreflect.order]
_ `|^sp` _ (order_scope) [in mathcomp.ssreflect.order]
_ `&^sp` _ (order_scope) [in mathcomp.ssreflect.order]
_ ><^sp _ (order_scope) [in mathcomp.ssreflect.order]
><^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
><^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ >=<^sp _ (order_scope) [in mathcomp.ssreflect.order]
>=<^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=<^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^sp _ ?= iff _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^sp _ ?= iff _ (order_scope) [in mathcomp.ssreflect.order]
_ <^sp _ <^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^sp _ <^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ <^sp _ <=^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^sp _ <=^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ >^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ <^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ >=^sp _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
_ <=^sp _ (order_scope) [in mathcomp.ssreflect.order]
>^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>^sp _ (order_scope) [in mathcomp.ssreflect.order]
<^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<^sp _ (order_scope) [in mathcomp.ssreflect.order]
>=^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
>=^sp _ (order_scope) [in mathcomp.ssreflect.order]
<=^sp _ :> _ (order_scope) [in mathcomp.ssreflect.order]
<=^sp _ (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]
{ 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]
_ .-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

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)