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

_

other

(79846 entries)

Notation 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

_

other

(1818 entries)

Binder 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

_

other

(48657 entries)

Module 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

_

other

(383 entries)

Variable 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

_

other

(4212 entries)

Library 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

_

other

(93 entries)

Lemma 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

_

other

(14712 entries)

Constructor 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

_

other

(223 entries)

Axiom 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

_

other

(45 entries)

Inductive 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

_

other

(132 entries)

Projection 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

_

other

(452 entries)

Section 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

_

other

(1429 entries)

Abbreviation 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

_

other

(1169 entries)

Definition 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

_

other

(6273 entries)

Record 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

_

other

(248 entries)

---

O

oAC [definition, in mathcomp.ssreflect.bigop]
oAC [section, in mathcomp.ssreflect.bigop]
oACE [lemma, in mathcomp.ssreflect.bigop]
oAC_com_law [definition, in mathcomp.ssreflect.bigop]
oAC_law [definition, in mathcomp.ssreflect.bigop]
oAC.op [variable, in mathcomp.ssreflect.bigop]
oAC.opA [variable, in mathcomp.ssreflect.bigop]
oAC.opC [variable, in mathcomp.ssreflect.bigop]
oAC.T [variable, in mathcomp.ssreflect.bigop]
oappEmap [lemma, in mathcomp.ssreflect.ssrfun]
oapp_comp_f [lemma, in mathcomp.ssreflect.ssrfun]
oapp_comp [lemma, in mathcomp.ssreflect.ssrfun]
obindEapp [lemma, in mathcomp.ssreflect.ssrfun]
ocan_in_comp [lemma, in mathcomp.ssreflect.ssrbool]
ocan_comp [lemma, in mathcomp.ssreflect.ssrfun]
odd [definition, in mathcomp.ssreflect.ssrnat]
oddB [lemma, in mathcomp.ssreflect.ssrnat]
oddb [lemma, in mathcomp.ssreflect.ssrnat]
oddD [lemma, in mathcomp.ssreflect.ssrnat]
oddM [lemma, in mathcomp.ssreflect.ssrnat]
oddN [lemma, in mathcomp.ssreflect.ssrnat]
oddS [lemma, in mathcomp.ssreflect.ssrnat]
oddSg [lemma, in mathcomp.solvable.pgroup]
oddX [lemma, in mathcomp.ssreflect.ssrnat]
odd_lift_perm [lemma, in mathcomp.fingroup.perm]
odd_permJ [lemma, in mathcomp.fingroup.perm]
odd_permV [lemma, in mathcomp.fingroup.perm]
odd_permM [lemma, in mathcomp.fingroup.perm]
odd_perm_prod [lemma, in mathcomp.fingroup.perm]
odd_tperm [lemma, in mathcomp.fingroup.perm]
odd_mul_tperm [lemma, in mathcomp.fingroup.perm]
odd_perm1 [lemma, in mathcomp.fingroup.perm]
odd_perm [definition, in mathcomp.fingroup.perm]
odd_mod [lemma, in mathcomp.ssreflect.div]
odd_gt2 [lemma, in mathcomp.ssreflect.ssrnat]
odd_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
odd_ltn [lemma, in mathcomp.ssreflect.ssrnat]
odd_geq [lemma, in mathcomp.ssreflect.ssrnat]
odd_uphalfK [lemma, in mathcomp.ssreflect.ssrnat]
odd_halfK [lemma, in mathcomp.ssreflect.ssrnat]
odd_double_half [lemma, in mathcomp.ssreflect.ssrnat]
odd_double [lemma, in mathcomp.ssreflect.ssrnat]
odd_pgroup_odd [lemma, in mathcomp.solvable.pgroup]
odd_2'nat [lemma, in mathcomp.ssreflect.prime]
odd_prime_gt2 [lemma, in mathcomp.ssreflect.prime]
odd_pgroup_rank1_cyclic [lemma, in mathcomp.solvable.extremal]
odd_not_extremal2 [lemma, in mathcomp.solvable.extremal]
odd_polyMX [lemma, in mathcomp.algebra.poly]
odd_poly_linear [definition, in mathcomp.algebra.poly]
odd_poly_additive [definition, in mathcomp.algebra.poly]
odd_poly_is_linear [lemma, in mathcomp.algebra.poly]
odd_polyZ [lemma, in mathcomp.algebra.poly]
odd_polyD [lemma, in mathcomp.algebra.poly]
odd_polyC [lemma, in mathcomp.algebra.poly]
odd_polyE [lemma, in mathcomp.algebra.poly]
odd_poly [definition, in mathcomp.algebra.poly]
offset:108 [binder, in mathcomp.ssreflect.div]
offset:89 [binder, in mathcomp.ssreflect.div]
ofs:2351 [binder, in mathcomp.algebra.ssralg]
of_irrK [lemma, in mathcomp.character.vcharacter]
of_irr [definition, in mathcomp.character.vcharacter]
ohead [definition, in mathcomp.ssreflect.seq]
Ohm [definition, in mathcomp.solvable.abelian]
OhmE [lemma, in mathcomp.solvable.abelian]
OhmEabelian [lemma, in mathcomp.solvable.abelian]
OhmJ [lemma, in mathcomp.solvable.abelian]
OhmPredP [lemma, in mathcomp.solvable.abelian]
OhmProps [section, in mathcomp.solvable.abelian]
OhmProps.char [section, in mathcomp.solvable.abelian]
OhmProps.char.D [variable, in mathcomp.solvable.abelian]
OhmProps.char.G [variable, in mathcomp.solvable.abelian]
OhmProps.char.gT [variable, in mathcomp.solvable.abelian]
OhmProps.char.n [variable, in mathcomp.solvable.abelian]
OhmProps.char.rT [variable, in mathcomp.solvable.abelian]
OhmProps.Generic [section, in mathcomp.solvable.abelian]
OhmProps.Generic.gT [variable, in mathcomp.solvable.abelian]
OhmProps.Generic.n [variable, in mathcomp.solvable.abelian]
OhmProps.gT [variable, in mathcomp.solvable.abelian]
OhmS [lemma, in mathcomp.solvable.abelian]
Ohm_Mho_homocyclic [lemma, in mathcomp.solvable.abelian]
Ohm_leq [lemma, in mathcomp.solvable.abelian]
Ohm_normal [lemma, in mathcomp.solvable.abelian]
Ohm_char [lemma, in mathcomp.solvable.abelian]
Ohm_mgFun [definition, in mathcomp.solvable.abelian]
Ohm_gFun [definition, in mathcomp.solvable.abelian]
Ohm_igFun [definition, in mathcomp.solvable.abelian]
Ohm_dprod [lemma, in mathcomp.solvable.abelian]
Ohm_p_cycle [lemma, in mathcomp.solvable.abelian]
Ohm_cont [lemma, in mathcomp.solvable.abelian]
Ohm_id [lemma, in mathcomp.solvable.abelian]
Ohm_sub [lemma, in mathcomp.solvable.abelian]
Ohm_group [definition, in mathcomp.solvable.abelian]
Ohm0 [lemma, in mathcomp.solvable.abelian]
Ohm1 [lemma, in mathcomp.solvable.abelian]
Ohm1Eexponent [lemma, in mathcomp.solvable.abelian]
Ohm1Eprime [lemma, in mathcomp.solvable.abelian]
Ohm1_homocyclicP [lemma, in mathcomp.solvable.abelian]
Ohm1_cyclic_pgroup_prime [lemma, in mathcomp.solvable.abelian]
Ohm1_cent_max [lemma, in mathcomp.solvable.abelian]
Ohm1_eq1 [lemma, in mathcomp.solvable.abelian]
Ohm1_id [lemma, in mathcomp.solvable.abelian]
Ohm1_abelem [lemma, in mathcomp.solvable.abelian]
Ohm1_extraspecial_odd [lemma, in mathcomp.solvable.extraspecial]
Ohm1_cent_max_normal_abelem [lemma, in mathcomp.solvable.maximal]
Ohm1_stab_Ohm1_SCN_series [lemma, in mathcomp.solvable.maximal]
oi:22 [binder, in mathcomp.ssreflect.ssrAC]
olift [definition, in mathcomp.ssreflect.ssrfun]
olift_comp [lemma, in mathcomp.ssreflect.ssrfun]
omapEapp [lemma, in mathcomp.ssreflect.ssrfun]
omapEbind [lemma, in mathcomp.ssreflect.ssrfun]
omapK [lemma, in mathcomp.ssreflect.ssrfun]
omap_id [lemma, in mathcomp.ssreflect.ssrfun]
omap_comp [lemma, in mathcomp.ssreflect.ssrfun]
om0:45 [binder, in mathcomp.algebra.ssrnum]
om:50 [binder, in mathcomp.algebra.ssrnum]
oneg [definition, in mathcomp.fingroup.fingroup]
oneq [definition, in mathcomp.algebra.rat]
one_group [definition, in mathcomp.fingroup.fingroup]
one:1127 [binder, in mathcomp.algebra.ssralg]
one:208 [binder, in mathcomp.algebra.ssralg]
one:911 [binder, in mathcomp.ssreflect.finset]
on_card_preimset [lemma, in mathcomp.ssreflect.finset]
oop [abbreviation, in mathcomp.ssreflect.bigop]
oopA_subdef [lemma, in mathcomp.ssreflect.bigop]
oopC_subdef [lemma, in mathcomp.ssreflect.bigop]
oopx1_subdef [lemma, in mathcomp.ssreflect.bigop]
oop1x_subdef [lemma, in mathcomp.ssreflect.bigop]
opAC [abbreviation, in mathcomp.ssreflect.ssrAC]
opACl [abbreviation, in mathcomp.ssreflect.ssrAC]
opACof [abbreviation, in mathcomp.ssreflect.ssrAC]
opair_of_sumK [lemma, in mathcomp.ssreflect.choice]
opair_of_sum [definition, in mathcomp.ssreflect.choice]
opA':36 [binder, in mathcomp.ssreflect.bigop]
opA:33 [binder, in mathcomp.ssreflect.bigop]
opC':24 [binder, in mathcomp.ssreflect.bigop]
opC:22 [binder, in mathcomp.ssreflect.bigop]
opC:32 [binder, in mathcomp.ssreflect.bigop]
opL':19 [binder, in mathcomp.ssreflect.bigop]
opL:15 [binder, in mathcomp.ssreflect.bigop]
opL:21 [binder, in mathcomp.ssreflect.bigop]
opmA:16 [binder, in mathcomp.ssreflect.bigop]
opmC:23 [binder, in mathcomp.ssreflect.bigop]
opM':29 [binder, in mathcomp.ssreflect.bigop]
opm0:28 [binder, in mathcomp.ssreflect.bigop]
opm1:18 [binder, in mathcomp.ssreflect.bigop]
opM:26 [binder, in mathcomp.ssreflect.bigop]
opm:988 [binder, in mathcomp.algebra.matrix]
opm:989 [binder, in mathcomp.algebra.matrix]
opm:990 [binder, in mathcomp.algebra.matrix]
opm:991 [binder, in mathcomp.algebra.matrix]
opm:992 [binder, in mathcomp.algebra.matrix]
opm:993 [binder, in mathcomp.algebra.matrix]
opm:994 [binder, in mathcomp.algebra.matrix]
opm:995 [binder, in mathcomp.algebra.matrix]
opm:996 [binder, in mathcomp.algebra.matrix]
opp [definition, in mathcomp.solvable.burnside_app]
oppmx [definition, in mathcomp.algebra.matrix]
oppmx_key [lemma, in mathcomp.algebra.matrix]
oppq [definition, in mathcomp.algebra.rat]
oppq_frac [lemma, in mathcomp.algebra.rat]
oppq_def [definition, in mathcomp.algebra.rat]
oppq_subdef [definition, in mathcomp.algebra.rat]
oppr_itvcc [lemma, in mathcomp.algebra.interval]
oppr_itvoc [lemma, in mathcomp.algebra.interval]
oppr_itvco [lemma, in mathcomp.algebra.interval]
oppr_itvoo [lemma, in mathcomp.algebra.interval]
oppr_itv [lemma, in mathcomp.algebra.interval]
oppS:1635 [binder, in mathcomp.algebra.ssralg]
oppS:1645 [binder, in mathcomp.algebra.ssralg]
oppS:1652 [binder, in mathcomp.algebra.ssralg]
oppS:1662 [binder, in mathcomp.algebra.ssralg]
oppS:1667 [binder, in mathcomp.algebra.ssralg]
oppS:1671 [binder, in mathcomp.algebra.ssralg]
oppS:1678 [binder, in mathcomp.algebra.ssralg]
oppS:1684 [binder, in mathcomp.algebra.ssralg]
oppS:1691 [binder, in mathcomp.algebra.ssralg]
oppS:1801 [binder, in mathcomp.algebra.ssralg]
oppS:1830 [binder, in mathcomp.algebra.ssralg]
oppzD [definition, in mathcomp.algebra.ssrint]
oppz_add [abbreviation, in mathcomp.algebra.ssrint]
opp_block_mx [lemma, in mathcomp.algebra.matrix]
opp_col_mx [lemma, in mathcomp.algebra.matrix]
opp_row_mx [lemma, in mathcomp.algebra.matrix]
opp_isometry [lemma, in mathcomp.character.classfun]
opp_pair [definition, in mathcomp.algebra.ssralg]
opp_lfunE [lemma, in mathcomp.algebra.vector]
opp_lfun [definition, in mathcomp.algebra.vector]
opp_poly_unlockable [definition, in mathcomp.algebra.poly]
opp_poly [definition, in mathcomp.algebra.poly]
opp_poly_key [lemma, in mathcomp.algebra.poly]
opp_poly_def [definition, in mathcomp.algebra.poly]
OpsTheory [section, in mathcomp.ssreflect.fintype]
OpsTheory.EnumPick [section, in mathcomp.ssreflect.fintype]
OpsTheory.EnumPick.P [variable, in mathcomp.ssreflect.fintype]
OpsTheory.T [variable, in mathcomp.ssreflect.fintype]
OptionEqType [section, in mathcomp.ssreflect.eqtype]
OptionEqType.T [variable, in mathcomp.ssreflect.eqtype]
OptionFinType [section, in mathcomp.ssreflect.fintype]
OptionFinType.T [variable, in mathcomp.ssreflect.fintype]
option_countType [definition, in mathcomp.ssreflect.choice]
option_countMixin [definition, in mathcomp.ssreflect.choice]
option_choiceType [definition, in mathcomp.ssreflect.choice]
option_choiceMixin [definition, in mathcomp.ssreflect.choice]
option_finType [definition, in mathcomp.ssreflect.fintype]
option_finMixin [definition, in mathcomp.ssreflect.fintype]
option_enumP [lemma, in mathcomp.ssreflect.fintype]
option_enum [definition, in mathcomp.ssreflect.fintype]
option_eqType [definition, in mathcomp.ssreflect.eqtype]
option_eqMixin [definition, in mathcomp.ssreflect.eqtype]
opt_eqP [lemma, in mathcomp.ssreflect.eqtype]
opt_eq [definition, in mathcomp.ssreflect.eqtype]
op_Wedderburn_id [lemma, in mathcomp.character.mxrepresentation]
op':532 [binder, in mathcomp.ssreflect.ssrnat]
op0m:27 [binder, in mathcomp.ssreflect.bigop]
op1m:17 [binder, in mathcomp.ssreflect.bigop]
op1:12 [binder, in mathcomp.ssreflect.bigop]
op2:13 [binder, in mathcomp.ssreflect.bigop]
op:14 [binder, in mathcomp.ssreflect.bigop]
op:172 [binder, in mathcomp.character.inertia]
op:20 [binder, in mathcomp.ssreflect.bigop]
op:235 [binder, in mathcomp.ssreflect.bigop]
op:25 [binder, in mathcomp.ssreflect.bigop]
op:28 [binder, in mathcomp.algebra.zmodp]
op:2951 [binder, in mathcomp.ssreflect.bigop]
op:302 [binder, in mathcomp.algebra.ssrnum]
op:35 [binder, in mathcomp.algebra.zmodp]
op:474 [binder, in mathcomp.character.character]
op:498 [binder, in mathcomp.ssreflect.ssrnat]
op:519 [binder, in mathcomp.ssreflect.ssrnat]
op:531 [binder, in mathcomp.ssreflect.ssrnat]
op:722 [binder, in mathcomp.character.classfun]
op:966 [binder, in mathcomp.ssreflect.bigop]
op:975 [binder, in mathcomp.ssreflect.order]
op:988 [binder, in mathcomp.ssreflect.order]
op:99 [binder, in mathcomp.ssreflect.ssrAC]
orbit [definition, in mathcomp.fingroup.action]
orbit [definition, in mathcomp.ssreflect.fingraph]
Orbit [section, in mathcomp.ssreflect.fingraph]
orbitE [lemma, in mathcomp.fingroup.action]
orbitE [lemma, in mathcomp.ssreflect.fingraph]
orbitJ [lemma, in mathcomp.fingroup.action]
orbitJs [lemma, in mathcomp.fingroup.action]
orbitP [lemma, in mathcomp.fingroup.action]
orbitPcycle [lemma, in mathcomp.ssreflect.fingraph]
orbitR [lemma, in mathcomp.fingroup.action]
orbitRs [lemma, in mathcomp.fingroup.action]
orbit_morphim_actperm [lemma, in mathcomp.fingroup.action]
orbit_conjsg [lemma, in mathcomp.fingroup.action]
orbit_rcoset [lemma, in mathcomp.fingroup.action]
orbit_lcoset [lemma, in mathcomp.fingroup.action]
orbit_inv [lemma, in mathcomp.fingroup.action]
orbit_eq_mem [lemma, in mathcomp.fingroup.action]
orbit_actr [lemma, in mathcomp.fingroup.action]
orbit_act [lemma, in mathcomp.fingroup.action]
orbit_transl [lemma, in mathcomp.fingroup.action]
orbit_eqP [lemma, in mathcomp.fingroup.action]
orbit_trans [lemma, in mathcomp.fingroup.action]
orbit_sym [lemma, in mathcomp.fingroup.action]
orbit_stabilizer [lemma, in mathcomp.fingroup.action]
orbit_transversalP [lemma, in mathcomp.fingroup.action]
orbit_transversal [definition, in mathcomp.fingroup.action]
orbit_partition [lemma, in mathcomp.fingroup.action]
orbit_conjsg_in [lemma, in mathcomp.fingroup.action]
orbit_rcoset_in [lemma, in mathcomp.fingroup.action]
orbit_lcoset_in [lemma, in mathcomp.fingroup.action]
orbit_inv_in [lemma, in mathcomp.fingroup.action]
orbit_actr_in [lemma, in mathcomp.fingroup.action]
orbit_act_in [lemma, in mathcomp.fingroup.action]
orbit_in_transl [lemma, in mathcomp.fingroup.action]
orbit_in_eqP [lemma, in mathcomp.fingroup.action]
orbit_in_trans [lemma, in mathcomp.fingroup.action]
orbit_in_sym [lemma, in mathcomp.fingroup.action]
orbit_rel [abbreviation, in mathcomp.fingroup.action]
orbit_refl [lemma, in mathcomp.fingroup.action]
orbit_id [lemma, in mathcomp.ssreflect.fingraph]
orbit_rot_cycle [lemma, in mathcomp.ssreflect.fingraph]
orbit_uniq [lemma, in mathcomp.ssreflect.fingraph]
Orbit.f [variable, in mathcomp.ssreflect.fingraph]
Orbit.fconnect [section, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_undup.homo_f [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_undup.f_inj [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_undup.p_undup_uniq [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_undup.f_p [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_undup.p [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_undup [section, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_cons.f_p [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_cons.p [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_cons.x [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_cons [section, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.homo_f [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.f_inj [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.mem_cycle.p_x [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.mem_cycle.x [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.mem_cycle.Up [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.mem_cycle [section, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.f_p [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p.p [variable, in mathcomp.ssreflect.fingraph]
Orbit.fcycle_p [section, in mathcomp.ssreflect.fingraph]
Orbit.orbit_inj.symf [variable, in mathcomp.ssreflect.fingraph]
Orbit.orbit_inj.injf [variable, in mathcomp.ssreflect.fingraph]
Orbit.orbit_inj [section, in mathcomp.ssreflect.fingraph]
Orbit.orbit_in.injf [variable, in mathcomp.ssreflect.fingraph]
Orbit.orbit_in.f_in [variable, in mathcomp.ssreflect.fingraph]
Orbit.orbit_in.S [variable, in mathcomp.ssreflect.fingraph]
Orbit.orbit_in [section, in mathcomp.ssreflect.fingraph]
Orbit.T [variable, in mathcomp.ssreflect.fingraph]
orbit1P [lemma, in mathcomp.fingroup.action]
orb_addoid [definition, in mathcomp.ssreflect.bigop]
orb_muloid [definition, in mathcomp.ssreflect.bigop]
orb_comoid [definition, in mathcomp.ssreflect.bigop]
orb_monoid [definition, in mathcomp.ssreflect.bigop]
order [definition, in mathcomp.fingroup.fingroup]
Order [module, in mathcomp.ssreflect.order]
order [definition, in mathcomp.ssreflect.fingraph]
order [library]
orderC [definition, in mathcomp.field.algnum]
orderE [lemma, in mathcomp.fingroup.fingroup]
orderJ [lemma, in mathcomp.fingroup.fingroup]
orderM [lemma, in mathcomp.solvable.cyclic]
orderPcycle [lemma, in mathcomp.ssreflect.fingraph]
orderSpred [lemma, in mathcomp.ssreflect.fingraph]
OrderStepCycle [constructor, in mathcomp.ssreflect.fingraph]
OrderStepNoCycle [constructor, in mathcomp.ssreflect.fingraph]
orderV [lemma, in mathcomp.fingroup.fingroup]
orderXdiv [lemma, in mathcomp.solvable.cyclic]
orderXdvd [lemma, in mathcomp.solvable.cyclic]
orderXexp [lemma, in mathcomp.solvable.cyclic]
orderXgcd [lemma, in mathcomp.solvable.cyclic]
orderXpfactor [lemma, in mathcomp.solvable.cyclic]
orderXpnat [lemma, in mathcomp.solvable.cyclic]
orderXprime [lemma, in mathcomp.solvable.cyclic]
order_Zp1 [lemma, in mathcomp.algebra.zmodp]
order_gt1 [lemma, in mathcomp.fingroup.fingroup]
order_eq1 [lemma, in mathcomp.fingroup.fingroup]
order_gt0 [lemma, in mathcomp.fingroup.fingroup]
order_constt [lemma, in mathcomp.solvable.pgroup]
order_path_min [lemma, in mathcomp.ssreflect.path]
order_path_min_in [lemma, in mathcomp.ssreflect.path]
order_primeChar [lemma, in mathcomp.field.finfield]
order_injm [lemma, in mathcomp.fingroup.morphism]
order_set_finv [lemma, in mathcomp.ssreflect.fingraph]
order_finv [lemma, in mathcomp.ssreflect.fingraph]
order_id [lemma, in mathcomp.ssreflect.fingraph]
order_spec_cycle [inductive, in mathcomp.ssreflect.fingraph]
order_id_cycle [lemma, in mathcomp.ssreflect.fingraph]
order_cycle [lemma, in mathcomp.ssreflect.fingraph]
order_le_cycle [lemma, in mathcomp.ssreflect.fingraph]
order_set [definition, in mathcomp.ssreflect.fingraph]
order_gt0 [lemma, in mathcomp.ssreflect.fingraph]
order_inj_cyclic [lemma, in mathcomp.solvable.cyclic]
order_dvdG [lemma, in mathcomp.solvable.cyclic]
order_inf [lemma, in mathcomp.solvable.cyclic]
order_dvdn [lemma, in mathcomp.solvable.cyclic]
Order.arg_max [definition, in mathcomp.ssreflect.order]
Order.arg_min [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice [module, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory [module, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.BDistrLatticeTheory [section, in mathcomp.ssreflect.order]
\bot [notation, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.disjoint_lexUr [lemma, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.disjoint_lexUl [lemma, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.joins_disjoint [lemma, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.leU2E [lemma, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.leU2l_le [lemma, in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.leU2r_le [lemma, in mathcomp.ssreflect.order]
Order.BDistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.BDistrLattice.base2 [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.BDistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.BDistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.BDistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.BDistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.BDistrLattice.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.BDistrLattice.Exports.bDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ bDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.BDistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.BDistrLattice.nb_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.BDistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.BDistrLattice.type [record, in mathcomp.ssreflect.order]
Order.BLattice [module, in mathcomp.ssreflect.order]
Order.BLatticeSyntax [module, in mathcomp.ssreflect.order]
\join_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\bot (order_scope) [notation, in mathcomp.ssreflect.order]
0%O [notation, in mathcomp.ssreflect.order]
Order.BLatticeTheory [module, in mathcomp.ssreflect.order]
Order.BLatticeTheory.BLatticeTheory [section, in mathcomp.ssreflect.order]
\bot [notation, in mathcomp.ssreflect.order]
Order.BLatticeTheory.Eq0NotPOs [constructor, in mathcomp.ssreflect.order]
Order.BLatticeTheory.eq0_xor_gt0 [inductive, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joinsP [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joinsP_seq [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_seq [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_setU [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_le [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_min [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_sup [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_min_seq [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joins_sup_seq [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.joinx0 [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.join_comoid [definition, in mathcomp.ssreflect.order]
Order.BLatticeTheory.join_monoid [definition, in mathcomp.ssreflect.order]
Order.BLatticeTheory.join_eq0 [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.join0x [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.lex0 [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.le_joins [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.le0x [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.ltx0 [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.lt0x [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.meetx0 [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.meet0x [lemma, in mathcomp.ssreflect.order]
Order.BLatticeTheory.POsNotEq0 [constructor, in mathcomp.ssreflect.order]
Order.BLatticeTheory.posxP [lemma, in mathcomp.ssreflect.order]
Order.BLattice.base [projection, in mathcomp.ssreflect.order]
Order.BLattice.bottom [projection, in mathcomp.ssreflect.order]
Order.BLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.BLattice.class [definition, in mathcomp.ssreflect.order]
Order.BLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.BLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.BLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.BLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.BLattice.class_of [record, in mathcomp.ssreflect.order]
Order.BLattice.clone [definition, in mathcomp.ssreflect.order]
Order.BLattice.clone_with [definition, in mathcomp.ssreflect.order]
Order.BLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.BLattice.Exports [module, in mathcomp.ssreflect.order]
Order.BLattice.Exports.BLatticeType [abbreviation, in mathcomp.ssreflect.order]
Order.BLattice.Exports.bLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ bLatticeType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ bLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ bLatticeType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ bLatticeType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.BLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.BLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.BLattice.mixin_of [record, in mathcomp.ssreflect.order]
Order.BLattice.pack [definition, in mathcomp.ssreflect.order]
Order.BLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.BLattice.sort [projection, in mathcomp.ssreflect.order]
Order.BLattice.type [record, in mathcomp.ssreflect.order]
Order.BoolOrder [module, in mathcomp.ssreflect.order]
Order.BoolOrder.andbE [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.andEbool [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.anti [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.BoolOrder [section, in mathcomp.ssreflect.order]
Order.BoolOrder.bool_display [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.complEbool [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports [module, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports.andEbool [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports.complEbool [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports.leEbool [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports.ltEbool [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports.orEbool [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.Exports.subEbool [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.finOrderType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.joinIB [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.leEbool [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.ltEbool [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.ltn_def [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.orbE [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.orderMixin [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.orEbool [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.sub [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.subEbool [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.subKI [lemma, in mathcomp.ssreflect.order]
Order.BoolOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.BoolOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.bottom [definition, in mathcomp.ssreflect.order]
Order.BottomMixin [module, in mathcomp.ssreflect.order]
Order.BottomMixin.bLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.BottomMixin.bottom [projection, in mathcomp.ssreflect.order]
Order.BottomMixin.BottomMixin [section, in mathcomp.ssreflect.order]
Order.BottomMixin.BottomMixin.disp [variable, in mathcomp.ssreflect.order]
Order.BottomMixin.BottomMixin.T [variable, in mathcomp.ssreflect.order]
Order.BottomMixin.Exports [module, in mathcomp.ssreflect.order]
Order.BottomMixin.Exports.BottomMixin [abbreviation, in mathcomp.ssreflect.order]
Order.BottomMixin.Exports.bottomMixin [abbreviation, in mathcomp.ssreflect.order]
Order.BottomMixin.le0x [projection, in mathcomp.ssreflect.order]
Order.BottomMixin.of_ [record, in mathcomp.ssreflect.order]
Order.CanMixin [module, in mathcomp.ssreflect.order]
Order.CanMixin.anti [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.disp [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.disp' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.f [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.f_mono [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.f_can [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.f' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.f'_can [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.DistrLattice.T' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.disp [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.disp' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.f [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.f_mono [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.f_can [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.f' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.f'_can [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.T [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Lattice.T' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.disp [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Partial [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Partial.f [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Partial.PCan [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Partial.PCan.f_can [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Partial.PCan.f' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Partial.T' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.T [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.f [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.PCan [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.PCan.f_can [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.PCan.f' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.PCan.total_le [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.PCan.T_porderType [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Order.Total.T' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Total [section, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Total.disp [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Total.disp' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Total.f [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Total.T [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanMixin.Total.T' [variable, in mathcomp.ssreflect.order]
Order.CanMixin.CanOrder [definition, in mathcomp.ssreflect.order]
Order.CanMixin.CanPOrder [definition, in mathcomp.ssreflect.order]
Order.CanMixin.Exports [module, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.CanOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.CanPOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.IsoDistrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.IsoLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.MonoTotalMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.PcanOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.Exports.PcanPOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CanMixin.IsoDistrLattice [definition, in mathcomp.ssreflect.order]
Order.CanMixin.IsoLattice [definition, in mathcomp.ssreflect.order]
Order.CanMixin.join [definition, in mathcomp.ssreflect.order]
Order.CanMixin.joinA [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.joinC [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.joinKI [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.le [definition, in mathcomp.ssreflect.order]
Order.CanMixin.lt [definition, in mathcomp.ssreflect.order]
Order.CanMixin.lt_def [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.meet [definition, in mathcomp.ssreflect.order]
Order.CanMixin.meetA [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.meetC [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.meetKI [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.meetUl [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.meet_eql [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.MonoTotal [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.PcanOrder [definition, in mathcomp.ssreflect.order]
Order.CanMixin.PcanPOrder [definition, in mathcomp.ssreflect.order]
Order.CanMixin.refl [lemma, in mathcomp.ssreflect.order]
Order.CanMixin.trans [lemma, in mathcomp.ssreflect.order]
Order.cardE [lemma, in mathcomp.ssreflect.order]
Order.cardT [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLattice [module, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin [module, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.cbDistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.CBDistrLatticeMixin [section, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.CBDistrLatticeMixin.disp [variable, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.CBDistrLatticeMixin.T [variable, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.Exports [module, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.Exports.CBDistrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.Exports.cbDistrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.joinIB [projection, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.of_ [record, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.sub [projection, in mathcomp.ssreflect.order]
Order.CBDistrLatticeMixin.subKI [projection, in mathcomp.ssreflect.order]
Order.CBDistrLatticeSyntax [module, in mathcomp.ssreflect.order]
_ `\` _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory [module, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.CBDistrLatticeTheory [section, in mathcomp.ssreflect.order]
\bot [notation, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_subr [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_subl [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_leC [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_le [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.eq_sub [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBI [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBIC [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBK [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBKC [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinIB [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinIBC [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinxB [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBKU [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBl [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBLR [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBr [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBRL [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBUK [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leB2 [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.lt0B [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetBI [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetBx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetIB [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetxB [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meet_eq0E_sub [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subBx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subIK [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subIx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subKI [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subKU [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subUK [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subUx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subxB [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subxI [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subxU [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subxx [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.subx0 [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.sub_eq0 [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.sub0x [lemma, in mathcomp.ssreflect.order]
Order.CBDistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.CBDistrLattice.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.CBDistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.CBDistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.CBDistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.CBDistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.CBDistrLattice.clone [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.clone_with [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.CBDistrLattice.Exports.CBDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
Order.CBDistrLattice.Exports.cbDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ cbDistrLatticeType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.CBDistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.CBDistrLattice.mixin_of [record, in mathcomp.ssreflect.order]
Order.CBDistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.CBDistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.CBDistrLattice.sub [projection, in mathcomp.ssreflect.order]
Order.CBDistrLattice.type [record, in mathcomp.ssreflect.order]
Order.comparable [definition, in mathcomp.ssreflect.order]
Order.compare [inductive, in mathcomp.ssreflect.order]
Order.CompareEq [constructor, in mathcomp.ssreflect.order]
Order.CompareGt [constructor, in mathcomp.ssreflect.order]
Order.comparel [inductive, in mathcomp.ssreflect.order]
Order.ComparelEq [constructor, in mathcomp.ssreflect.order]
Order.ComparelGt [constructor, in mathcomp.ssreflect.order]
Order.ComparelLt [constructor, in mathcomp.ssreflect.order]
Order.CompareLt [constructor, in mathcomp.ssreflect.order]
Order.compl [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice [module, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin [module, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.compl [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.complE [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.ctbDistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.CTBDistrLatticeMixin [section, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.CTBDistrLatticeMixin.disp [variable, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.CTBDistrLatticeMixin.sub [variable, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.CTBDistrLatticeMixin.T [variable, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.Exports [module, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.Exports.CTBDistrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.Exports.ctbDistrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeMixin.of_ [record, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeSyntax [module, in mathcomp.ssreflect.order]
~` _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory [module, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complB [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complE [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complI [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complK [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complU [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl_meets [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl_joins [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl_inj [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl0 [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl1 [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.CTBDistrLatticeTheory [section, in mathcomp.ssreflect.order]
\bot [notation, in mathcomp.ssreflect.order]
\top [notation, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.disj_leC [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.joinCx [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.joinxC [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.leBC [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.leC [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.leCx [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.lexC [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.meetCx [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.meetxC [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.subE [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.sub1x [lemma, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.base2 [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.cb_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.cb_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.clone [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.clone_with [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.compl [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.Exports.CTBDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.Exports.ctbDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ default_ctbDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ ctbDistrLatticeType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.mixin_of [record, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.mixin1 [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.mixin2 [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.CTBDistrLattice.type [record, in mathcomp.ssreflect.order]
Order.CTheory [module, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder [module, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.DefaultProdLexiOrder [section, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_finOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_orderType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdLexiOrder.prodlexi_porderType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder [module, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.DefaultProdOrder [section, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultProdOrder.prod_porderType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder [module, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.DefaultSeqLexiOrder [section, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.seqlexi_orderType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.seqlexi_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.seqlexi_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.seqlexi_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.seqlexi_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqLexiOrder.seqlexi_porderType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder [module, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder.DefaultSeqProdOrder [section, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder.seqprod_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder.seqprod_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder.seqprod_ndbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder.seqprod_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSeqProdOrder.seqprod_porderType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder [module, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.DefaultSetSubsetOrder [section, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultSetSubsetOrder.subset_porderType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder [module, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.DefaultTupleLexiOrder [section, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_finOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_orderType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleLexiOrder.tlexi_porderType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder [module, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.DefaultTupleProdOrder [section, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_latticeType [definition, in mathcomp.ssreflect.order]
Order.DefaultTupleProdOrder.tprod_porderType [definition, in mathcomp.ssreflect.order]
Order.DistrLattice [module, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin [module, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.DistrLatticeMixin [section, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.DistrLatticeMixin.disp [variable, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.DistrLatticeMixin.T [variable, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.Exports [module, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.Exports.DistrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.Exports.distrLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.meetUl [projection, in mathcomp.ssreflect.order]
Order.DistrLatticeMixin.of_ [record, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin [module, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.DistrLatticePOrderMixin [section, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.DistrLatticePOrderMixin.disp [variable, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.DistrLatticePOrderMixin.m [variable, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.DistrLatticePOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.Exports.DistrLatticeOfPOrderType [definition, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.Exports.DistrLatticePOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.Exports.distrLatticePOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.join [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.joinA [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.joinC [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.joinKI [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.leEmeet [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.meet [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.meetA [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.meetC [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.meetKU [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.meetUl [projection, in mathcomp.ssreflect.order]
Order.DistrLatticePOrderMixin.of_ [record, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory [module, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.DistrLatticeTheory [section, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.DistrLatticeTheory.L [variable, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.dual_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.dual_distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.joinIl [lemma, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.joinIr [lemma, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.meetUl [lemma, in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.meetUr [lemma, in mathcomp.ssreflect.order]
Order.DistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.DistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.DistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.DistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.DistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.DistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.DistrLattice.clone [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.clone_with [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.DistrLattice.Exports.DistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
Order.DistrLattice.Exports.distrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ distrLatticeType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ distrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ distrLatticeType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ distrLatticeType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.DistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.DistrLattice.mixin_of [record, in mathcomp.ssreflect.order]
Order.DistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.DistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.DistrLattice.type [record, in mathcomp.ssreflect.order]
Order.dual [definition, in mathcomp.ssreflect.order]
Order.DualLattice [module, in mathcomp.ssreflect.order]
Order.DualLattice.DualLattice [section, in mathcomp.ssreflect.order]
Order.DualLattice.DualLattice.L [variable, in mathcomp.ssreflect.order]
Order.DualLattice.dual_latticeType [definition, in mathcomp.ssreflect.order]
Order.DualLattice.dual_latticeMixin [definition, in mathcomp.ssreflect.order]
Order.DualLattice.dual_leEmeet [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinA [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinC [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinEdual [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinIK [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinIKC [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinKI [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.joinKIC [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.leEjoin [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.leEmeet [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetA [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetC [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetEdual [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetKU [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetKUC [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetUK [lemma, in mathcomp.ssreflect.order]
Order.DualLattice.meetUKC [lemma, in mathcomp.ssreflect.order]
Order.DualOrder [module, in mathcomp.ssreflect.order]
Order.DualOrder.DualOrder [section, in mathcomp.ssreflect.order]
Order.DualOrder.DualOrderTheory [section, in mathcomp.ssreflect.order]
Order.DualOrder.DualOrder.O [variable, in mathcomp.ssreflect.order]
Order.DualOrder.dual_finOrderType [definition, in mathcomp.ssreflect.order]
Order.DualOrder.dual_orderType [definition, in mathcomp.ssreflect.order]
Order.DualOrder.dual_totalMixin [lemma, in mathcomp.ssreflect.order]
Order.DualOrder.nth_count_eq [lemma, in mathcomp.ssreflect.order]
Order.DualOrder.nth_count_gt [lemma, in mathcomp.ssreflect.order]
Order.DualOrder.nth_count_ge [lemma, in mathcomp.ssreflect.order]
Order.DualOrder.sorted_filter_ge [lemma, in mathcomp.ssreflect.order]
Order.DualOrder.sorted_filter_gt [lemma, in mathcomp.ssreflect.order]
Order.DualPOrder [module, in mathcomp.ssreflect.order]
Order.DualPOrder.DualPOrder [section, in mathcomp.ssreflect.order]
Order.DualPOrder.DualPOrder.T [variable, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_porderType [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_porderMixin [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_le_anti [lemma, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_lt_def [lemma, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_finType [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_countType [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_choiceType [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.dual_eqType [definition, in mathcomp.ssreflect.order]
Order.DualPOrder.leEdual [lemma, in mathcomp.ssreflect.order]
Order.DualPOrder.ltEdual [lemma, in mathcomp.ssreflect.order]
Order.DualSyntax [module, in mathcomp.ssreflect.order]
Order.DualSyntax.join [abbreviation, in mathcomp.ssreflect.order]
Order.DualSyntax.meet [abbreviation, in mathcomp.ssreflect.order]
><^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=<^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<?<=^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<?=^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<=^d%O (fun_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^d_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^d_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\top^d (order_scope) [notation, in mathcomp.ssreflect.order]
\bot^d (order_scope) [notation, in mathcomp.ssreflect.order]
_ `|^d` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ `&^d` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ ><^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
><^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
><^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=<^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=<^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=<^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^d _ ?<= if _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^d _ ?<= if _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^d _ ?= iff _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^d _ ?= iff _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^d _ <^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^d _ <^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^d _ <=^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^d _ <=^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
>^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
<^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
<=^d _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<=^d _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ ^d (type_scope) [notation, in mathcomp.ssreflect.order]
0^d%O [notation, in mathcomp.ssreflect.order]
1^d%O [notation, in mathcomp.ssreflect.order]
\bot [notation, in mathcomp.ssreflect.order]
\top [notation, in mathcomp.ssreflect.order]
Order.DualTBDistrLattice [module, in mathcomp.ssreflect.order]
Order.DualTBDistrLattice.DualTBDistrLattice [section, in mathcomp.ssreflect.order]
Order.DualTBDistrLattice.dual_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DualTBDistrLattice.dual_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DualTBDistrLattice.dual_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.DualTBLattice [module, in mathcomp.ssreflect.order]
Order.DualTBLattice.botEdual [lemma, in mathcomp.ssreflect.order]
Order.DualTBLattice.DualTBLattice [section, in mathcomp.ssreflect.order]
Order.DualTBLattice.dual_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.DualTBLattice.dual_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.DualTBLattice.dual_tbLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.DualTBLattice.dual_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.DualTBLattice.dual_bLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.DualTBLattice.lex1 [lemma, in mathcomp.ssreflect.order]
Order.DualTBLattice.topEdual [lemma, in mathcomp.ssreflect.order]
Order.dual_top [abbreviation, in mathcomp.ssreflect.order]
Order.dual_bottom [abbreviation, in mathcomp.ssreflect.order]
Order.dual_join [abbreviation, in mathcomp.ssreflect.order]
Order.dual_meet [abbreviation, in mathcomp.ssreflect.order]
Order.dual_min [abbreviation, in mathcomp.ssreflect.order]
Order.dual_max [abbreviation, in mathcomp.ssreflect.order]
Order.dual_lteif [abbreviation, in mathcomp.ssreflect.order]
Order.dual_leif [abbreviation, in mathcomp.ssreflect.order]
Order.dual_gt [abbreviation, in mathcomp.ssreflect.order]
Order.dual_ge [abbreviation, in mathcomp.ssreflect.order]
Order.dual_comparable [abbreviation, in mathcomp.ssreflect.order]
Order.dual_lt [abbreviation, in mathcomp.ssreflect.order]
Order.dual_le [abbreviation, in mathcomp.ssreflect.order]
Order.dual_display [definition, in mathcomp.ssreflect.order]
Order.DvdSyntax [module, in mathcomp.ssreflect.order]
Order.DvdSyntax.dvd [abbreviation, in mathcomp.ssreflect.order]
Order.DvdSyntax.gcd [abbreviation, in mathcomp.ssreflect.order]
Order.DvdSyntax.lcm [abbreviation, in mathcomp.ssreflect.order]
Order.DvdSyntax.nat0 [abbreviation, in mathcomp.ssreflect.order]
Order.DvdSyntax.nat1 [abbreviation, in mathcomp.ssreflect.order]
Order.DvdSyntax.sdvd [abbreviation, in mathcomp.ssreflect.order]
@ lcm _ (fun_scope) [notation, in mathcomp.ssreflect.order]
@ gcd _ (fun_scope) [notation, in mathcomp.ssreflect.order]
@ sdvd _ (fun_scope) [notation, in mathcomp.ssreflect.order]
@ dvd _ (fun_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\lcm_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\gcd_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ %<| _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ %| _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.dvd_display [lemma, in mathcomp.ssreflect.order]
Order.Enum [section, in mathcomp.ssreflect.order]
Order.enum [abbreviation, in mathcomp.ssreflect.order]
Order.enumT [lemma, in mathcomp.ssreflect.order]
Order.EnumVal [module, in mathcomp.ssreflect.order]
Order.EnumVal.EnumVal [section, in mathcomp.ssreflect.order]
Order.EnumVal.EnumVal.d [variable, in mathcomp.ssreflect.order]
Order.EnumVal.EnumVal.T [variable, in mathcomp.ssreflect.order]
Order.EnumVal.EnumVal.total [section, in mathcomp.ssreflect.order]
Order.EnumVal.EnumVal.total.leT_total [variable, in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_bij [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_bij [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_in_inj [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_bij_in [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_inj [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_inj [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_valK [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_valK_in [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rankK [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rankK_in [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_nth [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_valP [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.enum_val [definition, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank [definition, in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_in [definition, in mathcomp.ssreflect.order]
Order.EnumVal.eq_enum_rank_in [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.le_enum_rank [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.le_enum_rank_in [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.le_enum_val [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.nth_enum_rank [lemma, in mathcomp.ssreflect.order]
Order.EnumVal.nth_enum_rank_in [lemma, in mathcomp.ssreflect.order]
Order.enum_val_bij [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rank_bij [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rank_in_inj [abbreviation, in mathcomp.ssreflect.order]
Order.enum_val_bij_in [abbreviation, in mathcomp.ssreflect.order]
Order.enum_val_inj [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rank_inj [abbreviation, in mathcomp.ssreflect.order]
Order.enum_valK [abbreviation, in mathcomp.ssreflect.order]
Order.enum_valK_in [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rankK [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rankK_in [abbreviation, in mathcomp.ssreflect.order]
Order.enum_val_nth [abbreviation, in mathcomp.ssreflect.order]
Order.enum_valP [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rank [abbreviation, in mathcomp.ssreflect.order]
Order.enum_rank_in [abbreviation, in mathcomp.ssreflect.order]
Order.enum_val [abbreviation, in mathcomp.ssreflect.order]
Order.enum_ord [lemma, in mathcomp.ssreflect.order]
Order.enum_set1 [lemma, in mathcomp.ssreflect.order]
Order.enum_setT [lemma, in mathcomp.ssreflect.order]
Order.enum_set0 [lemma, in mathcomp.ssreflect.order]
Order.enum_uniq [lemma, in mathcomp.ssreflect.order]
Order.Enum.d [variable, in mathcomp.ssreflect.order]
Order.Enum.T [variable, in mathcomp.ssreflect.order]
Order.enum0 [lemma, in mathcomp.ssreflect.order]
Order.enum1 [lemma, in mathcomp.ssreflect.order]
Order.eq_enum_rank_in [abbreviation, in mathcomp.ssreflect.order]
Order.eq_cardT [lemma, in mathcomp.ssreflect.order]
Order.eq_enum [lemma, in mathcomp.ssreflect.order]
Order.FinCDistrLattice [module, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.base2 [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.countType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.count_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.count_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.Exports.finCDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ finCDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finDistrLattice_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finDistrLattice_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finLattice_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finLattice_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finPOrder_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finPOrder_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.finType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.fin_ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.fin_cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinCDistrLattice.type [record, in mathcomp.ssreflect.order]
Order.FinDistrLattice [module, in mathcomp.ssreflect.order]
Order.FinDistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.FinDistrLattice.base2 [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.FinDistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.FinDistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.FinDistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.FinDistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.FinDistrLattice.countType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.count_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.count_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.count_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.FinDistrLattice.Exports.finDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ finDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finLattice_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finLattice_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finLattice_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finPOrder_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finPOrder_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finPOrder_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.finType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.fin_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.fin_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.fin_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.FinDistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.FinDistrLattice.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinDistrLattice.type [record, in mathcomp.ssreflect.order]
Order.FinLattice [module, in mathcomp.ssreflect.order]
Order.FinLattice.base [projection, in mathcomp.ssreflect.order]
Order.FinLattice.base2 [definition, in mathcomp.ssreflect.order]
Order.FinLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.class [definition, in mathcomp.ssreflect.order]
Order.FinLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.FinLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.FinLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.FinLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.FinLattice.class_of [record, in mathcomp.ssreflect.order]
Order.FinLattice.countType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.count_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.count_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.count_latticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.Exports [module, in mathcomp.ssreflect.order]
Order.FinLattice.Exports.finLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ finLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.FinLattice.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.finPOrder_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.finPOrder_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.finPOrder_latticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.finType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.fin_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.fin_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.fin_latticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.FinLattice.pack [definition, in mathcomp.ssreflect.order]
Order.FinLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.sort [projection, in mathcomp.ssreflect.order]
Order.FinLattice.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinLattice.type [record, in mathcomp.ssreflect.order]
Order.FinPOrder [module, in mathcomp.ssreflect.order]
Order.FinPOrder.base [projection, in mathcomp.ssreflect.order]
Order.FinPOrder.base2 [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.class [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.ClassDef [section, in mathcomp.ssreflect.order]
Order.FinPOrder.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.FinPOrder.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.FinPOrder.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.FinPOrder.class_of [record, in mathcomp.ssreflect.order]
Order.FinPOrder.countType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.count_porderType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.Exports [module, in mathcomp.ssreflect.order]
Order.FinPOrder.Exports.finPOrderType [abbreviation, in mathcomp.ssreflect.order]
[ finPOrderType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.FinPOrder.finType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.fin_porderType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.mixin [projection, in mathcomp.ssreflect.order]
Order.FinPOrder.pack [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.FinPOrder.sort [projection, in mathcomp.ssreflect.order]
Order.FinPOrder.type [record, in mathcomp.ssreflect.order]
Order.FinTotal [module, in mathcomp.ssreflect.order]
Order.FinTotal.base [projection, in mathcomp.ssreflect.order]
Order.FinTotal.base2 [definition, in mathcomp.ssreflect.order]
Order.FinTotal.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.choiceType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.class [definition, in mathcomp.ssreflect.order]
Order.FinTotal.ClassDef [section, in mathcomp.ssreflect.order]
Order.FinTotal.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.FinTotal.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.FinTotal.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.FinTotal.class_of [record, in mathcomp.ssreflect.order]
Order.FinTotal.countType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.eqType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.Exports [module, in mathcomp.ssreflect.order]
Order.FinTotal.Exports.finOrderType [abbreviation, in mathcomp.ssreflect.order]
[ finOrderType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.FinTotal.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.finType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.latticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.mixin [projection, in mathcomp.ssreflect.order]
Order.FinTotal.orderType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_finLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_bLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_finPOrderType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_finType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.order_countType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.pack [definition, in mathcomp.ssreflect.order]
Order.FinTotal.porderType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.sort [projection, in mathcomp.ssreflect.order]
Order.FinTotal.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.FinTotal.type [record, in mathcomp.ssreflect.order]
Order.ge [definition, in mathcomp.ssreflect.order]
Order.GelNotLt [constructor, in mathcomp.ssreflect.order]
Order.GeNotLt [constructor, in mathcomp.ssreflect.order]
Order.gt [definition, in mathcomp.ssreflect.order]
Order.GtlNotLe [constructor, in mathcomp.ssreflect.order]
Order.GtNotLe [constructor, in mathcomp.ssreflect.order]
Order.InCompare [constructor, in mathcomp.ssreflect.order]
Order.incompare [inductive, in mathcomp.ssreflect.order]
Order.InCompareEq [constructor, in mathcomp.ssreflect.order]
Order.InCompareGt [constructor, in mathcomp.ssreflect.order]
Order.InComparel [constructor, in mathcomp.ssreflect.order]
Order.incomparel [inductive, in mathcomp.ssreflect.order]
Order.InComparelEq [constructor, in mathcomp.ssreflect.order]
Order.InComparelGt [constructor, in mathcomp.ssreflect.order]
Order.InComparelLt [constructor, in mathcomp.ssreflect.order]
Order.InCompareLt [constructor, in mathcomp.ssreflect.order]
Order.index_enum_ord [lemma, in mathcomp.ssreflect.order]
Order.join [definition, in mathcomp.ssreflect.order]
Order.Lattice [module, in mathcomp.ssreflect.order]
Order.LatticeDef [section, in mathcomp.ssreflect.order]
Order.LatticeMixin [module, in mathcomp.ssreflect.order]
Order.LatticeMixin.Exports [module, in mathcomp.ssreflect.order]
Order.LatticeMixin.Exports.LatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LatticeMixin.Exports.latticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LatticeMixin.join [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.joinA [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.joinC [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.joinKI [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.LatticeMixin.LatticeMixin [section, in mathcomp.ssreflect.order]
Order.LatticeMixin.LatticeMixin.disp [variable, in mathcomp.ssreflect.order]
Order.LatticeMixin.LatticeMixin.T [variable, in mathcomp.ssreflect.order]
Order.LatticeMixin.leEmeet [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.meet [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.meetA [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.meetC [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.meetKU [projection, in mathcomp.ssreflect.order]
Order.LatticeMixin.of_ [record, in mathcomp.ssreflect.order]
Order.LatticeSyntax [module, in mathcomp.ssreflect.order]
_ `|` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ `&` _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin [module, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.eq_joinr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.eq_joinl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinAC [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinACA [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinCA [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinKU [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinKUC [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinUK [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinUKC [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.joinxx [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.join_r [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.join_l [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.join_idPl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.join_idPr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.LatticeTheoryJoin [section, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lcomparableP [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lcomparable_ltP [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lcomparable_leP [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lcomparable_ltgtP [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.leUidl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.leUidr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.leUl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.leUr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.leUx [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.leU2 [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lexUl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lexUr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryJoin.lexU2 [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet [module, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.eq_meetr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.eq_meetl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.LatticeTheoryMeet [section, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIidl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIidr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIxl [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIxr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leIx2 [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.leI2 [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.lexI [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetAC [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetACA [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetCA [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetIK [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetIKC [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetKI [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetKIC [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meetxx [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meet_r [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meet_l [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meet_idPr [lemma, in mathcomp.ssreflect.order]
Order.LatticeTheoryMeet.meet_idPl [lemma, in mathcomp.ssreflect.order]
Order.Lattice.base [projection, in mathcomp.ssreflect.order]
Order.Lattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.Lattice.class [definition, in mathcomp.ssreflect.order]
Order.Lattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.Lattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.Lattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.Lattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.Lattice.class_of [record, in mathcomp.ssreflect.order]
Order.Lattice.clone [definition, in mathcomp.ssreflect.order]
Order.Lattice.clone_with [definition, in mathcomp.ssreflect.order]
Order.Lattice.eqType [definition, in mathcomp.ssreflect.order]
Order.Lattice.Exports [module, in mathcomp.ssreflect.order]
Order.Lattice.Exports.LatticeType [abbreviation, in mathcomp.ssreflect.order]
Order.Lattice.Exports.latticeType [abbreviation, in mathcomp.ssreflect.order]
[ latticeType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ latticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ latticeType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ latticeType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.Lattice.join [projection, in mathcomp.ssreflect.order]
Order.Lattice.meet [projection, in mathcomp.ssreflect.order]
Order.Lattice.mixin [projection, in mathcomp.ssreflect.order]
Order.Lattice.mixin_of [record, in mathcomp.ssreflect.order]
Order.Lattice.pack [definition, in mathcomp.ssreflect.order]
Order.Lattice.porderType [definition, in mathcomp.ssreflect.order]
Order.Lattice.sort [projection, in mathcomp.ssreflect.order]
Order.Lattice.type [record, in mathcomp.ssreflect.order]
Order.le [definition, in mathcomp.ssreflect.order]
Order.leif [definition, in mathcomp.ssreflect.order]
Order.LelNotGt [constructor, in mathcomp.ssreflect.order]
Order.lel_xor_gt [inductive, in mathcomp.ssreflect.order]
Order.LeNotGt [constructor, in mathcomp.ssreflect.order]
Order.LeOrderMixin [module, in mathcomp.ssreflect.order]
Order.LeOrderMixin.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.LeOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.LeOrderMixin.Exports.LeOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LeOrderMixin.Exports.leOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LeOrderMixin.Exports.OrderOfChoiceType [definition, in mathcomp.ssreflect.order]
Order.LeOrderMixin.join [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.joinA [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.joinC [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.joinE [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.joinKI [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.join_def [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.le [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.LeOrderMixin [section, in mathcomp.ssreflect.order]
Order.LeOrderMixin.LeOrderMixin.m [variable, in mathcomp.ssreflect.order]
Order.LeOrderMixin.LeOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.LeOrderMixin.LeOrderMixin.T_distrLatticeType [variable, in mathcomp.ssreflect.order]
Order.LeOrderMixin.LeOrderMixin.T_orderType [variable, in mathcomp.ssreflect.order]
Order.LeOrderMixin.lePOrderMixin [definition, in mathcomp.ssreflect.order]
Order.LeOrderMixin.le_def [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.le_refl [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.le_total [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.le_trans [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.le_anti [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.lt [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.lt_def [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meet [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meetA [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meetC [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meetE [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meetKU [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meetUl [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meetxx [lemma, in mathcomp.ssreflect.order]
Order.LeOrderMixin.meet_def [projection, in mathcomp.ssreflect.order]
Order.LeOrderMixin.of_ [record, in mathcomp.ssreflect.order]
Order.LeOrderMixin.totalMixin [definition, in mathcomp.ssreflect.order]
Order.LePOrderMixin [module, in mathcomp.ssreflect.order]
Order.LePOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.LePOrderMixin.Exports.LePOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LePOrderMixin.Exports.lePOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LePOrderMixin.le [projection, in mathcomp.ssreflect.order]
Order.LePOrderMixin.LePOrderMixin [section, in mathcomp.ssreflect.order]
Order.LePOrderMixin.LePOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.LePOrderMixin.lexx [projection, in mathcomp.ssreflect.order]
Order.LePOrderMixin.le_trans [projection, in mathcomp.ssreflect.order]
Order.LePOrderMixin.le_anti [projection, in mathcomp.ssreflect.order]
Order.LePOrderMixin.lt [projection, in mathcomp.ssreflect.order]
Order.LePOrderMixin.lt_def [projection, in mathcomp.ssreflect.order]
Order.LePOrderMixin.of_ [record, in mathcomp.ssreflect.order]
Order.LePOrderMixin.porderMixin [definition, in mathcomp.ssreflect.order]
Order.LexiSyntax [module, in mathcomp.ssreflect.order]
Order.LexiSyntax.joinlexi [abbreviation, in mathcomp.ssreflect.order]
Order.LexiSyntax.meetlexi [abbreviation, in mathcomp.ssreflect.order]
><^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=<^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<?=^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<=^l%O (fun_scope) [notation, in mathcomp.ssreflect.order]
_ `|^l` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ `&^l` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ ><^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
><^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
><^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=<^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=<^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=<^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^l _ ?= iff _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^l _ ?= iff _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^l _ <^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^l _ <^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^l _ <=^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^l _ <=^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
>^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
<^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
<=^l _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<=^l _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.lexi_display [lemma, in mathcomp.ssreflect.order]
Order.le_enum_rank [abbreviation, in mathcomp.ssreflect.order]
Order.le_enum_rank_in [abbreviation, in mathcomp.ssreflect.order]
Order.le_enum_val [abbreviation, in mathcomp.ssreflect.order]
Order.le_xor_gt [inductive, in mathcomp.ssreflect.order]
Order.le_of_leif [definition, in mathcomp.ssreflect.order]
Order.lt [definition, in mathcomp.ssreflect.order]
Order.lteif [definition, in mathcomp.ssreflect.order]
Order.LTheory [module, in mathcomp.ssreflect.order]
Order.LtlNotGe [constructor, in mathcomp.ssreflect.order]
Order.ltl_xor_ge [inductive, in mathcomp.ssreflect.order]
Order.LtNotGe [constructor, in mathcomp.ssreflect.order]
Order.LtOrderMixin [module, in mathcomp.ssreflect.order]
Order.LtOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.LtOrderMixin.Exports.LtOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LtOrderMixin.Exports.ltOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LtOrderMixin.join [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.join_def_le [lemma, in mathcomp.ssreflect.order]
Order.LtOrderMixin.join_def [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.le [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.le_total [lemma, in mathcomp.ssreflect.order]
Order.LtOrderMixin.le_trans [lemma, in mathcomp.ssreflect.order]
Order.LtOrderMixin.le_anti [lemma, in mathcomp.ssreflect.order]
Order.LtOrderMixin.le_def [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.lt [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.LtOrderMixin [section, in mathcomp.ssreflect.order]
Order.LtOrderMixin.LtOrderMixin.m [variable, in mathcomp.ssreflect.order]
Order.LtOrderMixin.LtOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.LtOrderMixin.lt_def [lemma, in mathcomp.ssreflect.order]
Order.LtOrderMixin.lt_total [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.lt_trans [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.lt_irr [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.meet [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.meet_def_le [lemma, in mathcomp.ssreflect.order]
Order.LtOrderMixin.meet_def [projection, in mathcomp.ssreflect.order]
Order.LtOrderMixin.of_ [record, in mathcomp.ssreflect.order]
Order.LtOrderMixin.orderMixin [definition, in mathcomp.ssreflect.order]
Order.LtPOrderMixin [module, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.Exports.LtPOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.Exports.ltPOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.le [projection, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.lePOrderMixin [definition, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.le_trans [lemma, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.le_anti [lemma, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.le_refl [lemma, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.le_def [projection, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.lt [projection, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.LtPOrderMixin [section, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.LtPOrderMixin.m [variable, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.LtPOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.lt_def [lemma, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.lt_asym [lemma, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.lt_trans [projection, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.lt_irr [projection, in mathcomp.ssreflect.order]
Order.LtPOrderMixin.of_ [record, in mathcomp.ssreflect.order]
Order.lt_xor_ge [inductive, in mathcomp.ssreflect.order]
Order.max [definition, in mathcomp.ssreflect.order]
Order.max_fun [definition, in mathcomp.ssreflect.order]
Order.meet [definition, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin [module, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.Exports [module, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.Exports.MeetJoinLeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.Exports.meetJoinLeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.join [projection, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.joinA [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.joinC [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.joinKI [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.joinP [projection, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.join_leR [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.join_leL [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.join_lel [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.leEmeet [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meet [projection, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meetA [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meetC [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.MeetJoinLeMixin [section, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.MeetJoinLeMixin.disp [variable, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.MeetJoinLeMixin.m [variable, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.MeetJoinLeMixin.T [variable, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meetKU [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meetP [projection, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meet_leR [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meet_leL [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.meet_lel [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinLeMixin.of_ [record, in mathcomp.ssreflect.order]
Order.MeetJoinMixin [module, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.Exports [module, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.Exports.DistrLatticeOfChoiceType [definition, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.Exports.MeetJoinMixin [abbreviation, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.Exports.meetJoinMixin [abbreviation, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.join [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.joinA [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.joinC [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.joinKI [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.le [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.le_trans [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.le_anti [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.le_refl [lemma, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.le_def [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.lt [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.lt_def [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.meet [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.meetA [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.meetC [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.MeetJoinMixin [section, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.MeetJoinMixin.m [variable, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.MeetJoinMixin.T [variable, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.MeetJoinMixin.T_porderType [variable, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.meetKU [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.meetUl [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.meetxx [projection, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.of_ [record, in mathcomp.ssreflect.order]
Order.MeetJoinMixin.porderMixin [definition, in mathcomp.ssreflect.order]
Order.mem_enum [lemma, in mathcomp.ssreflect.order]
Order.min [definition, in mathcomp.ssreflect.order]
Order.min_fun [definition, in mathcomp.ssreflect.order]
Order.mono_unique [lemma, in mathcomp.ssreflect.order]
Order.mono_sorted_enum [lemma, in mathcomp.ssreflect.order]
Order.NatDvd [module, in mathcomp.ssreflect.order]
Order.NatDvd.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.choiceType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.countType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.dvdE [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.eqType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.Exports [module, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.dvdEnat [definition, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.gcdEnat [definition, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.lcmEnat [definition, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.natdvd [abbreviation, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.nat0E [definition, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.nat1E [definition, in mathcomp.ssreflect.order]
Order.NatDvd.Exports.sdvdEnat [definition, in mathcomp.ssreflect.order]
Order.NatDvd.gcdE [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.joinKI [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.latticeType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.lcmE [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.lcmnn [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.le_def [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.meetKU [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.meetUl [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.NatDvd [section, in mathcomp.ssreflect.order]
Order.NatDvd.nat0E [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.nat1E [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.porderType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.sdvdE [lemma, in mathcomp.ssreflect.order]
Order.NatDvd.t [definition, in mathcomp.ssreflect.order]
Order.NatDvd.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatDvd.t_distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory [module, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.decnP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.decn_inP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.homo_ltn_lt [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.homo_ltn_lt_in [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.incnP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.incn_inP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.NatMonotonyTheory [section, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.NatMonotonyTheory.D [variable, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.NatMonotonyTheory.Dconvex [variable, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.NatMonotonyTheory.f [variable, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nhomo_ltn_lt [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nhomo_ltn_lt_in [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nondecnP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nondecn_inP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nonincnP [lemma, in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nonincn_inP [lemma, in mathcomp.ssreflect.order]
Order.NatOrder [module, in mathcomp.ssreflect.order]
Order.NatOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatOrder.botEnat [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.NatOrder.Exports [module, in mathcomp.ssreflect.order]
Order.NatOrder.Exports.botEnat [definition, in mathcomp.ssreflect.order]
Order.NatOrder.Exports.leEnat [definition, in mathcomp.ssreflect.order]
Order.NatOrder.Exports.ltEnat [definition, in mathcomp.ssreflect.order]
Order.NatOrder.Exports.maxEnat [definition, in mathcomp.ssreflect.order]
Order.NatOrder.Exports.minEnat [definition, in mathcomp.ssreflect.order]
Order.NatOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.NatOrder.leEnat [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.ltEnat [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.ltn_def [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.maxEnat [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.minEnat [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.NatOrder [section, in mathcomp.ssreflect.order]
Order.NatOrder.nat_display [lemma, in mathcomp.ssreflect.order]
Order.NatOrder.orderMixin [definition, in mathcomp.ssreflect.order]
Order.NatOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.NatOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.nth_enum_rank [abbreviation, in mathcomp.ssreflect.order]
Order.nth_enum_rank_in [abbreviation, in mathcomp.ssreflect.order]
Order.nth_ord_enum [lemma, in mathcomp.ssreflect.order]
Order.nth_enum_ord [lemma, in mathcomp.ssreflect.order]
Order.Ordinal [section, in mathcomp.ssreflect.order]
Order.OrdinalOrder [module, in mathcomp.ssreflect.order]
Order.OrdinalOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.botEord [lemma, in mathcomp.ssreflect.order]
Order.OrdinalOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.Exports [module, in mathcomp.ssreflect.order]
Order.OrdinalOrder.Exports.botEord [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.Exports.leEord [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.Exports.ltEord [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.Exports.topEord [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.finOrderType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.leEord [lemma, in mathcomp.ssreflect.order]
Order.OrdinalOrder.ltEord [lemma, in mathcomp.ssreflect.order]
Order.OrdinalOrder.orderMixin [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.OrdinalOrder [section, in mathcomp.ssreflect.order]
Order.OrdinalOrder.OrdinalOrder.NonTrivial [section, in mathcomp.ssreflect.order]
Order.OrdinalOrder.OrdinalOrder.NonTrivial.n [variable, in mathcomp.ssreflect.order]
Order.OrdinalOrder.OrdinalOrder.NonTrivial.n' [variable, in mathcomp.ssreflect.order]
Order.OrdinalOrder.OrdinalOrder.PossiblyTrivial [section, in mathcomp.ssreflect.order]
Order.OrdinalOrder.OrdinalOrder.PossiblyTrivial.n [variable, in mathcomp.ssreflect.order]
Order.OrdinalOrder.ord_display [lemma, in mathcomp.ssreflect.order]
Order.OrdinalOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.OrdinalOrder.topEord [lemma, in mathcomp.ssreflect.order]
Order.POCoercions [module, in mathcomp.ssreflect.order]
Order.POrder [module, in mathcomp.ssreflect.order]
Order.POrderDef [section, in mathcomp.ssreflect.order]
Order.POrderDef.disp [variable, in mathcomp.ssreflect.order]
Order.POrderDef.LiftedPOrder [section, in mathcomp.ssreflect.order]
Order.POrderDef.LiftedPOrder.T' [variable, in mathcomp.ssreflect.order]
Order.POrderDef.T [variable, in mathcomp.ssreflect.order]
_ >< _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=< _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.POrderTheory [module, in mathcomp.ssreflect.order]
Order.POrderTheory.bigmax_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.bigmax_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparableP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparablexx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_lt_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_le_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_ltn_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_ltn_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_leq_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_leq_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraFlt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraFle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_not_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_not_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraNlt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraNle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraPlt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraPle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraTlt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraTle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_bigr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_bigl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_arg_maxP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_arg_minP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_min_maxr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_max_minr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxACA [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minACA [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxCA [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minCA [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxAC [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minAC [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_min_maxl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_max_minl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxA [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minA [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_maxl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_maxr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_minl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_minr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteifNE [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxKx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxxK [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minKx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minxK [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_gt_max [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lt_max [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ge_max [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_le_max [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_gt_min [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lt_min [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ge_min [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_le_min [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_max_idPl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_min_idPr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_eq_maxl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_eq_minr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxC [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minC [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxEge [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minEge [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxEgt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minEgt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_sym [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ltP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_leP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ltgtP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ltNge [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_leNgt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ContraTheory [section, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_lt_ltn [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_lt_leq [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_le_ltn [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_le_leq [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_ltF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_leF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_lt_not [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_le_not [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_ltN [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_leN [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_ltT [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.contra_leT [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.count_lt_le_mem [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.count_le_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.count_lt_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.dec_inj_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.dec_inj [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.eqTleif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.eq_maxr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.eq_minl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.eq_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.eq_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.filter_le_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.filter_lt_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.geE [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ge_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ge_comparable [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ge_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ge_anti [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ge_refl [definition, in mathcomp.ssreflect.order]
Order.POrderTheory.gtE [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.gt_comparable [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.gt_eqF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.incomparable_ltF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.incomparable_leF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.incomparable_eqF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.inc_inj_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.inc_inj [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.inj_nhomo_lt_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.inj_homo_lt_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.inj_nhomo_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.inj_homo_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leifP [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leif_eq [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leif_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leif_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leif_refl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leW_nmono_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leW_mono_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leW_nmono [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.leW_mono [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lexx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_bigmin [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_comparable [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_eq [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_leq_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_ltn_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_filter [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_mask [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_filter [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_mask [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_pairwise [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_pairwise [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_sortedE [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_min [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_lt_asym [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_gtF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_lt_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_eqVlt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_le_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_anti [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.le_refl [definition, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifN [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifNF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifS [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifT [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifW [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteifxx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_imply [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_andb [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_orb [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_anti [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltexx [definition, in mathcomp.ssreflect.order]
Order.POrderTheory.lte_anti [definition, in mathcomp.ssreflect.order]
Order.POrderTheory.ltNleif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltrW_lteif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltW [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_nhomo_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_homo_in [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_nhomo [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_homo [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.ltxx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_bigmin [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_comparable [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_eq [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_uniq [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_ltn_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_leq_nth [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_filter [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_mask [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_filter [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_mask [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_uniq_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_pairwise [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_pairwise [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_sortedE [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_min [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_le_asym [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_leAnge [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_gtF [definition, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_geF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_asym [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_nsym [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_le_trans [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_eqF [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_irreflexive [definition, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_neqAle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.lt_def [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.maxEle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.maxElt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.maxxx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.max_maxxK [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.max_maxKx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.max_idPr [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.max_r [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.max_l [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.minEle [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.minElt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.minxx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.min_minxK [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.min_minKx [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.min_idPl [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.min_r [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.min_l [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.mono_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.mono_in_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.nmono_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.nmono_in_leif [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.nth_count_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.nth_count_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory [section, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory.D [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory.D' [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory.f [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory.ge_antiT [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory.leT_anti [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderMonotonyTheory.leT'_anti [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory [section, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.ArgExtremum [section, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.ArgExtremum.F_comparable [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax [section, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax.f [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax.I [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax.P [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax.r [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax.x [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.bigminmax.x0 [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable2 [section, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable2.cmp_xy [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable2.x [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable2.y [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable2.z [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3 [section, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.cmp_yz [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.cmp_xz [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.cmp_xy [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.P [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.x [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.y [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.POrderTheory.Comparable3.z [variable, in mathcomp.ssreflect.order]
Order.POrderTheory.sorted_filter_le [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.sorted_filter_lt [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.sort_lt_id [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.sort_le_id [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_lt_sorted [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_le_sorted [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_lt_path [lemma, in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_le_path [lemma, in mathcomp.ssreflect.order]
Order.POrder.base [projection, in mathcomp.ssreflect.order]
Order.POrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.POrder.class [definition, in mathcomp.ssreflect.order]
Order.POrder.ClassDef [section, in mathcomp.ssreflect.order]
Order.POrder.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.POrder.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.POrder.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.POrder.class_of [record, in mathcomp.ssreflect.order]
Order.POrder.clone [definition, in mathcomp.ssreflect.order]
Order.POrder.clone_with [definition, in mathcomp.ssreflect.order]
Order.POrder.eqType [definition, in mathcomp.ssreflect.order]
Order.POrder.Exports [module, in mathcomp.ssreflect.order]
Order.POrder.Exports.POrderType [abbreviation, in mathcomp.ssreflect.order]
Order.POrder.Exports.porderType [abbreviation, in mathcomp.ssreflect.order]
[ porderType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ porderType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ porderType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ porderType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.POrder.le [projection, in mathcomp.ssreflect.order]
Order.POrder.lt [projection, in mathcomp.ssreflect.order]
Order.POrder.mixin [projection, in mathcomp.ssreflect.order]
Order.POrder.mixin_of [record, in mathcomp.ssreflect.order]
Order.POrder.pack [definition, in mathcomp.ssreflect.order]
Order.POrder.sort [projection, in mathcomp.ssreflect.order]
Order.POrder.type [record, in mathcomp.ssreflect.order]
Order.POSyntax [module, in mathcomp.ssreflect.order]
Order.POSyntax.leLHS [abbreviation, in mathcomp.ssreflect.order]
Order.POSyntax.leRHS [abbreviation, in mathcomp.ssreflect.order]
Order.POSyntax.ltLHS [abbreviation, in mathcomp.ssreflect.order]
Order.POSyntax.ltRHS [abbreviation, in mathcomp.ssreflect.order]
><%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=<%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<?<=%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<?=%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<=%O (fun_scope) [notation, in mathcomp.ssreflect.order]
_ \max _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ \min _ (order_scope) [notation, in mathcomp.ssreflect.order]
[ arg max_ ( _ > _ ) _ ] (order_scope) [notation, in mathcomp.ssreflect.order]
[ arg max_ ( _ > _ in _ ) _ ] (order_scope) [notation, in mathcomp.ssreflect.order]
[ arg max_ ( _ > _ | _ ) _ ] (order_scope) [notation, in mathcomp.ssreflect.order]
[ arg min_ ( _ < _ ) _ ] (order_scope) [notation, in mathcomp.ssreflect.order]
[ arg min_ ( _ < _ in _ ) _ ] (order_scope) [notation, in mathcomp.ssreflect.order]
[ arg min_ ( _ < _ | _ ) _ ] (order_scope) [notation, in mathcomp.ssreflect.order]
_ >< _ (order_scope) [notation, in mathcomp.ssreflect.order]
>< _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>< _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=< _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=< _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=< _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ ?<= if _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ ?<= if _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ ?= iff _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ ?= iff _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ < _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ < _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ <= _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ <= _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ > _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ > _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ < _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >= _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >= _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <= _ (order_scope) [notation, in mathcomp.ssreflect.order]
> _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
> _ (order_scope) [notation, in mathcomp.ssreflect.order]
< _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
< _ (order_scope) [notation, in mathcomp.ssreflect.order]
>= _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>= _ (order_scope) [notation, in mathcomp.ssreflect.order]
<= _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<= _ (order_scope) [notation, in mathcomp.ssreflect.order]
Order.ProdLexiOrder [module, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.anti [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.botEprodlexi [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.countType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports [module, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.botEprodlexi [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.leEprodlexi [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.lexi_pair [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.ltEprodlexi [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.ltxi_pair [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.sub_prod_lexi [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.Exports.topEprodlexi [definition, in mathcomp.ssreflect.order]
_ *l _ (type_scope) [notation, in mathcomp.ssreflect.order]
_ *lexi[ _ ] _ (type_scope) [notation, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.finOrderType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.finType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.le [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.leEprodlexi [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.lexi_pair [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.lex1 [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.le0x [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.lt [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ltEprodlexi [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ltxi_pair [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.lt_def [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder [section, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.FinDistrLattice [section, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.FinDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.FinDistrLattice.T' [variable, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.POrder [section, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.POrder.T [variable, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.POrder.T' [variable, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.Total [section, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.Total.T [variable, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ProdLexiOrder.Total.T' [variable, in mathcomp.ssreflect.order]
_ * _ (type_scope) [notation, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.refl [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.sub_prod_lexi [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.topEprodlexi [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.total [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.trans [lemma, in mathcomp.ssreflect.order]
Order.ProdLexiOrder.type [definition, in mathcomp.ssreflect.order]
Order.ProdOrder [module, in mathcomp.ssreflect.order]
Order.ProdOrder.anti [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.botEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.cbDistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.compl [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.complE [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.complEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.countType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.ctbDistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports [module, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.botEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.complEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.joinEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.leEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.le_pair [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.ltEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.lt_pair [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.meetEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.subEprod [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.Exports.topEprod [definition, in mathcomp.ssreflect.order]
_ *p _ (type_scope) [notation, in mathcomp.ssreflect.order]
_ *prod[ _ ] _ (type_scope) [notation, in mathcomp.ssreflect.order]
Order.ProdOrder.finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.finType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.join [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.joinA [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.joinC [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.joinEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.joinIB [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.joinKI [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.le [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.leEmeet [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.leEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.lex1 [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.le_pair [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.le0x [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.ltEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.lt_pair [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.meet [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.meetA [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.meetC [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.meetEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.meetKU [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.meetUl [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.BLattice [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.BLattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.BLattice.T' [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.CBDistrLattice [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.CBDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.CBDistrLattice.T' [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.CTBDistrLattice [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.CTBDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.CTBDistrLattice.T' [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.DistrLattice [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.DistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.DistrLattice.T' [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.Lattice [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.Lattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.Lattice.T' [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.POrder [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.POrder.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.POrder.T' [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.TBLattice [section, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.TBLattice.T [variable, in mathcomp.ssreflect.order]
Order.ProdOrder.ProdOrder.TBLattice.T' [variable, in mathcomp.ssreflect.order]
_ * _ (type_scope) [notation, in mathcomp.ssreflect.order]
Order.ProdOrder.refl [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.sub [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.subEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.subKI [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.ProdOrder.topEprod [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.trans [lemma, in mathcomp.ssreflect.order]
Order.ProdOrder.type [definition, in mathcomp.ssreflect.order]
Order.ProdSyntax [module, in mathcomp.ssreflect.order]
Order.ProdSyntax.join [abbreviation, in mathcomp.ssreflect.order]
Order.ProdSyntax.meet [abbreviation, in mathcomp.ssreflect.order]
><^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=<^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<?=^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
>=^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
<=^p%O (fun_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet^p_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\join^p_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ `|^p` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ `&^p` _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ ><^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
><^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
><^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=<^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=<^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=<^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^p _ ?= iff _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^p _ ?= iff _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^p _ <^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^p _ <^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^p _ <=^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^p _ <=^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ >=^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
_ <=^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
>^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
<^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
>=^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
<=^p _ :> _ (order_scope) [notation, in mathcomp.ssreflect.order]
<=^p _ (order_scope) [notation, in mathcomp.ssreflect.order]
\bot [notation, in mathcomp.ssreflect.order]
\top [notation, in mathcomp.ssreflect.order]
Order.prod_display [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder [module, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.anti [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.countType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.eqhead_ltxiE [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.eqhead_lexiE [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports [module, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.eqhead_ltxiE [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.eqhead_lexiE [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.leEseqlexi [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.lexis0 [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.lexi_lehead [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.lexi_cons [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.lexi0s [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.ltEseqltxi [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.ltxis0 [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.ltxi_lehead [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.ltxi_cons [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.ltxi0s [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.neqhead_ltxiE [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.neqhead_lexiE [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.seqlexi [abbreviation, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.seqlexi_with [abbreviation, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.Exports.sub_seqprod_lexi [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.le [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.leEseqlexi [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexis0 [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexi_lehead [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexi_cons [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexi0s [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lt [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltEseqlexi [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxis0 [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxi_lehead [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxi_cons [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxi0s [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lt_def [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.neqhead_ltxiE [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.neqhead_lexiE [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.refl [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.seq [abbreviation, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.SeqLexiOrder [section, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.SeqLexiOrder.POrder [section, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.SeqLexiOrder.POrder.T [variable, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.SeqLexiOrder.Total [section, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.SeqLexiOrder.Total.T [variable, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.sub_seqprod_lexi [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.total [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.trans [lemma, in mathcomp.ssreflect.order]
Order.SeqLexiOrder.type [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder [module, in mathcomp.ssreflect.order]
Order.SeqProdOrder.anti [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.botEseq [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.countType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports [module, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.botEseq [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.joinEseq [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.leEseq [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.les0 [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.le_cons [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.le0s [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.meetEseq [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.meet_cons [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.seqprod [abbreviation, in mathcomp.ssreflect.order]
Order.SeqProdOrder.Exports.seqprod_with [abbreviation, in mathcomp.ssreflect.order]
Order.SeqProdOrder.join [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.joinA [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.joinC [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.joinEseq [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.joinKI [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.join_cons [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.le [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.leEmeet [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.leEseq [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.les0 [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.le_cons [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.le0s [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meet [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetA [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetC [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetEseq [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetKU [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetss [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetUl [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.meet_cons [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.SeqProdOrder.refl [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.seq [abbreviation, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder [section, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder.DistrLattice [section, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder.DistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder.Lattice [section, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder.Lattice.T [variable, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder.POrder [section, in mathcomp.ssreflect.order]
Order.SeqProdOrder.SeqProdOrder.POrder.T [variable, in mathcomp.ssreflect.order]
Order.SeqProdOrder.trans [lemma, in mathcomp.ssreflect.order]
Order.SeqProdOrder.type [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder [module, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.botEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.complEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.countType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports [module, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.botEsubset [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.complEsubset [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.joinEsubset [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.leEsubset [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.meetEsubset [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.subEsubset [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.Exports.topEsubset [definition, in mathcomp.ssreflect.order]
{ subset _ } (type_scope) [notation, in mathcomp.ssreflect.order]
{ subset [ _ ] _ } (type_scope) [notation, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.finType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.joinEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.leEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.le_def [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.meetEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setIDv [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setKIC [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setKUC [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.SetSubsetOrder [section, in mathcomp.ssreflect.order]
{ subset _ } [notation, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setTDsym [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.subEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.subset_display [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.topEsubset [lemma, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.type [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.type_of [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.t_ctbdistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.t_cbdistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.SetSubsetOrder.t_distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.set_enum [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder [module, in mathcomp.ssreflect.order]
Order.SigmaOrder.anti [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.botEsig [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports [module, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.botEsig [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.leEsig [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.le_Taggedr [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.le_Taggedl [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.ltEsig [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.lt_Taggedr [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.lt_Taggedl [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.Exports.topEsig [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.finOrderType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.le [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.leEsig [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.lex1 [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.le_Taggedr [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.le_Taggedl [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.le0x [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.lt [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.ltEsig [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.lt_Taggedr [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.lt_Taggedl [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.lt_def [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.refl [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder [section, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.FinDistrLattice [section, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.FinDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.FinDistrLattice.T' [variable, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.POrder [section, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.POrder.T [variable, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.POrder.T' [variable, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.Total [section, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.Total.T [variable, in mathcomp.ssreflect.order]
Order.SigmaOrder.SigmaOrder.Total.T' [variable, in mathcomp.ssreflect.order]
Order.SigmaOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.SigmaOrder.topEsig [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.total [lemma, in mathcomp.ssreflect.order]
Order.SigmaOrder.trans [lemma, in mathcomp.ssreflect.order]
Order.size_enum_ord [lemma, in mathcomp.ssreflect.order]
Order.sub [definition, in mathcomp.ssreflect.order]
Order.SubOrder [module, in mathcomp.ssreflect.order]
Order.SubOrder.Exports [module, in mathcomp.ssreflect.order]
Order.SubOrder.Exports.leEsub [definition, in mathcomp.ssreflect.order]
Order.SubOrder.Exports.ltEsub [definition, in mathcomp.ssreflect.order]
[ totalOrderMixin of _ by <: ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ porderMixin of _ by <: ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.SubOrder.leEsub [lemma, in mathcomp.ssreflect.order]
Order.SubOrder.ltEsub [lemma, in mathcomp.ssreflect.order]
Order.SubOrder.Partial [section, in mathcomp.ssreflect.order]
Order.SubOrder.sub_OrderType [definition, in mathcomp.ssreflect.order]
Order.SubOrder.sub_DistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.SubOrder.sub_LatticeType [definition, in mathcomp.ssreflect.order]
Order.SubOrder.sub_TotalOrderMixin [definition, in mathcomp.ssreflect.order]
Order.SubOrder.sub_POrderType [definition, in mathcomp.ssreflect.order]
Order.SubOrder.sub_POrderMixin [definition, in mathcomp.ssreflect.order]
Order.SubOrder.Total [section, in mathcomp.ssreflect.order]
Order.Syntax [module, in mathcomp.ssreflect.order]
Order.TBDistrLattice [module, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory [module, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.cover_leIxr [lemma, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.cover_leIxl [lemma, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.join_addoid [definition, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.leI2E [lemma, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.leI2l_le [lemma, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.leI2r_le [lemma, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.meets_total [lemma, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.meet_addoid [definition, in mathcomp.ssreflect.order]
Order.TBDistrLatticeTheory.TBDistrLatticeTheory [section, in mathcomp.ssreflect.order]
\top [notation, in mathcomp.ssreflect.order]
Order.TBDistrLattice.base [projection, in mathcomp.ssreflect.order]
Order.TBDistrLattice.base2 [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.class [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.TBDistrLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.TBDistrLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.TBDistrLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.TBDistrLattice.class_of [record, in mathcomp.ssreflect.order]
Order.TBDistrLattice.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.Exports [module, in mathcomp.ssreflect.order]
Order.TBDistrLattice.Exports.tbDistrLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ tbDistrLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.TBDistrLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.TBDistrLattice.ntb_bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.ntb_distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.pack [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.sort [projection, in mathcomp.ssreflect.order]
Order.TBDistrLattice.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBDistrLattice.type [record, in mathcomp.ssreflect.order]
Order.TBLattice [module, in mathcomp.ssreflect.order]
Order.TBLatticeSyntax [module, in mathcomp.ssreflect.order]
\meet_ ( _ in _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ in _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ <= _ < _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ <= _ < _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ : _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ : _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ _ _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ <- _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\meet_ ( _ <- _ | _ ) _ (order_scope) [notation, in mathcomp.ssreflect.order]
\top (order_scope) [notation, in mathcomp.ssreflect.order]
1%O [notation, in mathcomp.ssreflect.order]
Order.TBLatticeTheory [module, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.joinx1 [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.join_muloid [definition, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.join1x [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.le_meets [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.le1x [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meetsP [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meetsP_seq [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_seq [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_setU [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_ge [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_max [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_inf [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_max_seq [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meets_inf_seq [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meetx1 [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meet_muloid [definition, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meet_comoid [definition, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meet_monoid [definition, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meet_eq1 [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.meet1x [lemma, in mathcomp.ssreflect.order]
Order.TBLatticeTheory.TBLatticeTheory [section, in mathcomp.ssreflect.order]
\top [notation, in mathcomp.ssreflect.order]
Order.TBLattice.base [projection, in mathcomp.ssreflect.order]
Order.TBLattice.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.TBLattice.choiceType [definition, in mathcomp.ssreflect.order]
Order.TBLattice.class [definition, in mathcomp.ssreflect.order]
Order.TBLattice.ClassDef [section, in mathcomp.ssreflect.order]
Order.TBLattice.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.TBLattice.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.TBLattice.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.TBLattice.class_of [record, in mathcomp.ssreflect.order]
Order.TBLattice.clone [definition, in mathcomp.ssreflect.order]
Order.TBLattice.clone_with [definition, in mathcomp.ssreflect.order]
Order.TBLattice.eqType [definition, in mathcomp.ssreflect.order]
Order.TBLattice.Exports [module, in mathcomp.ssreflect.order]
Order.TBLattice.Exports.TBLatticeType [abbreviation, in mathcomp.ssreflect.order]
Order.TBLattice.Exports.tbLatticeType [abbreviation, in mathcomp.ssreflect.order]
[ tbLatticeType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ tbLatticeType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ tbLatticeType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ tbLatticeType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.TBLattice.latticeType [definition, in mathcomp.ssreflect.order]
Order.TBLattice.mixin [projection, in mathcomp.ssreflect.order]
Order.TBLattice.mixin_of [record, in mathcomp.ssreflect.order]
Order.TBLattice.pack [definition, in mathcomp.ssreflect.order]
Order.TBLattice.porderType [definition, in mathcomp.ssreflect.order]
Order.TBLattice.sort [projection, in mathcomp.ssreflect.order]
Order.TBLattice.top [projection, in mathcomp.ssreflect.order]
Order.TBLattice.type [record, in mathcomp.ssreflect.order]
Order.Theory [module, in mathcomp.ssreflect.order]
Order.top [definition, in mathcomp.ssreflect.order]
Order.TopMixin [module, in mathcomp.ssreflect.order]
Order.TopMixin.Exports [module, in mathcomp.ssreflect.order]
Order.TopMixin.Exports.TopMixin [abbreviation, in mathcomp.ssreflect.order]
Order.TopMixin.Exports.topMixin [abbreviation, in mathcomp.ssreflect.order]
Order.TopMixin.lex1 [projection, in mathcomp.ssreflect.order]
Order.TopMixin.of_ [record, in mathcomp.ssreflect.order]
Order.TopMixin.tbLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.TopMixin.top [projection, in mathcomp.ssreflect.order]
Order.TopMixin.TopMixin [section, in mathcomp.ssreflect.order]
Order.TopMixin.TopMixin.disp [variable, in mathcomp.ssreflect.order]
Order.TopMixin.TopMixin.T [variable, in mathcomp.ssreflect.order]
Order.Total [module, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin [module, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.Exports [module, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.Exports.OrderOfLattice [definition, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.Exports.totalLatticeMixin [abbreviation, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.meetUl [lemma, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.of_ [definition, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.TotalLatticeMixin [section, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.TotalLatticeMixin.comparableT [variable, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.TotalLatticeMixin.disp [variable, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.TotalLatticeMixin.m [variable, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.TotalLatticeMixin.T [variable, in mathcomp.ssreflect.order]
Order.TotalLatticeMixin.totalMixin [definition, in mathcomp.ssreflect.order]
Order.TotalOrderMixin [module, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.Exports.totalOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.of_ [definition, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.totalOrderMixin [definition, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.TotalOrderMixin [section, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.TotalOrderMixin.disp [variable, in mathcomp.ssreflect.order]
Order.TotalOrderMixin.TotalOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin [module, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.Exports [module, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.Exports.OrderOfPOrder [definition, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.Exports.totalPOrderMixin [abbreviation, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.join [definition, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.joinA [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.joinC [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.joinKI [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.leEmeet [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.leP [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.ltgtP [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.meet [definition, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.meetA [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.meetC [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.meetKU [lemma, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.of_ [definition, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.totalLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.TotalPOrderMixin [section, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.TotalPOrderMixin.comparableT [variable, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.TotalPOrderMixin.disp [variable, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.TotalPOrderMixin.m [variable, in mathcomp.ssreflect.order]
Order.TotalPOrderMixin.TotalPOrderMixin.T [variable, in mathcomp.ssreflect.order]
Order.TotalTheory [module, in mathcomp.ssreflect.order]
Order.TotalTheory.arg_maxP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.arg_minP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxD1 [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxID [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_eq_arg [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_ltP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_leP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_sup [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_idr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_idl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_split [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_mkcond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigminD1 [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigminID [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_eq_arg [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_gtP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_geP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_inf [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_le_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_idr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_idl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_split [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_mkcond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.comparableT [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_lt_maxl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_lt_maxr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_le_maxl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_le_maxr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_lt_minr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_lt_minl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_le_minl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.comparable_le_minr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.contraFle [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contraFlt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contraNle [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contraNlt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contraPle [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contraPlt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ContraTheory [section, in mathcomp.ssreflect.order]
Order.TotalTheory.contraTle [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contraTlt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_lt_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_le_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_ltn_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_ltn_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_leq_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_leq_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_not_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.contra_not_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.count_lt_ge [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.count_le_gt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_bigmax [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_bigmin [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_maxl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_minr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_ltRL [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_ltLR [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_leRL [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.eq_leLR [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.filter_sort_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ge_max [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ge_min [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ge_total [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.gt_max [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.gt_min [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.joinEtotal [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.leIx [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.leNgt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.leP [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.lexU [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_minl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.le_minr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.le_maxr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.le_maxl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.le_nmono_in [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_mono_in [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_nmono [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_mono [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax2 [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin2 [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_ord_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_ord_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_ord [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_ord [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_nat_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_nat_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_nat [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_nat [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_max [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_min [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.le_total [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lteifNE [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_maxl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_maxr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_minl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_minr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lteIx [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.lteUx [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.ltexI [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.ltexU [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.ltgtP [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.ltIx [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ltNge [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ltP [definition, in mathcomp.ssreflect.order]
Order.TotalTheory.ltUx [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ltxI [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.ltxU [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_minl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_minr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_maxr [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_maxl [abbreviation, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_max [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_min [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.lt_total [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.mask_sort_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxA [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxAC [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxACA [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxC [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxCA [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxEge [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxEgt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxKx [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.maxxK [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.max_minr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.max_minl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.max_idPl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.meetEtotal [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.mem2_sort_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minA [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minAC [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minACA [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minC [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minCA [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minEge [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minEgt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minKx [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.minxK [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.min_maxr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.min_maxl [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.min_idPr [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.neq_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.perm_sort_leP [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sorted_subseq_sort_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sorted_mask_sort_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sort_lt_sorted [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sort_le_sorted [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.subseq_sort_le [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmax_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmin_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmax [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmin [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_in_bigmax [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_in_bigmin [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmax_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmin_cond [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmax_seq [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmin_seq [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmax [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmin [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory [section, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.D [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.f [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.leT_total [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.leT_anti [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.leT'_anti [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.ltT_def [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.ltT_neqAle [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalMonotonyTheory.ltT'_neqAle [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory [section, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.ArgExtremum [section, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_finType.x [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_finType.I [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_finType [section, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_Type.x [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_Type.r [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_Type.I [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.bigminmax_Type [section, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.ge_min_id [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.TotalTheory.le_max_id [variable, in mathcomp.ssreflect.order]
Order.TotalTheory.wlog_lt [lemma, in mathcomp.ssreflect.order]
Order.TotalTheory.wlog_le [lemma, in mathcomp.ssreflect.order]
Order.Total.base [projection, in mathcomp.ssreflect.order]
Order.Total.choiceType [definition, in mathcomp.ssreflect.order]
Order.Total.class [definition, in mathcomp.ssreflect.order]
Order.Total.ClassDef [section, in mathcomp.ssreflect.order]
Order.Total.ClassDef.cT [variable, in mathcomp.ssreflect.order]
Order.Total.ClassDef.disp [variable, in mathcomp.ssreflect.order]
Order.Total.ClassDef.T [variable, in mathcomp.ssreflect.order]
Order.Total.class_of [record, in mathcomp.ssreflect.order]
Order.Total.clone [definition, in mathcomp.ssreflect.order]
Order.Total.clone_with [definition, in mathcomp.ssreflect.order]
Order.Total.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.Total.eqType [definition, in mathcomp.ssreflect.order]
Order.Total.Exports [module, in mathcomp.ssreflect.order]
Order.Total.Exports.OrderType [abbreviation, in mathcomp.ssreflect.order]
Order.Total.Exports.orderType [abbreviation, in mathcomp.ssreflect.order]
[ orderType of _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ orderType of _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ orderType of _ for _ with _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
[ orderType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.order]
Order.Total.latticeType [definition, in mathcomp.ssreflect.order]
Order.Total.mixin [projection, in mathcomp.ssreflect.order]
Order.Total.mixin_of [definition, in mathcomp.ssreflect.order]
Order.Total.pack [definition, in mathcomp.ssreflect.order]
Order.Total.porderType [definition, in mathcomp.ssreflect.order]
Order.Total.sort [projection, in mathcomp.ssreflect.order]
Order.Total.type [record, in mathcomp.ssreflect.order]
Order.TTheory [module, in mathcomp.ssreflect.order]
Order.TupleLexiOrder [module, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.botEtlexi [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.countType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports [module, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports.botEtlexi [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports.lexi_tupleP [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports.ltxi_tuplePlt [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports.ltxi_tupleP [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports.sub_tprod_lexi [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.Exports.topEtlexi [definition, in mathcomp.ssreflect.order]
_ .-tuplelexi (type_scope) [notation, in mathcomp.ssreflect.order]
_ .-tuplelexi[ _ ] (type_scope) [notation, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.finOrderType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.finType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.lexi_tupleP [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.lex1 [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.le0x [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.ltxi_tuplePlt [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.ltxi_tupleP [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.orderType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.sub_tprod_lexi [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.topEtlexi [lemma, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.total [definition, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder [section, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.Basics [section, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.Basics.n [variable, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.BDistrLattice [section, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.BDistrLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.BDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.POrder [section, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.TBDistrLattice [section, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.TBDistrLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.TBDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.Total [section, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.Total.n [variable, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.TupleLexiOrder.Total.T [variable, in mathcomp.ssreflect.order]
_ .-tuple (type_scope) [notation, in mathcomp.ssreflect.order]
Order.TupleLexiOrder.type [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder [module, in mathcomp.ssreflect.order]
Order.TupleProdOrder.bDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.bLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.botEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.cbDistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.cbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.choiceType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.compl [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.complE [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.complEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.countType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.ctbDistrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.ctbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.distrLatticeMixin [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.distrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.eqType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports [module, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.botEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.complEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.joinEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.leEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.ltEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.meetEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.subEtprod [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.tnth_compl [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.tnth_sub [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.tnth_join [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.tnth_meet [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.Exports.topEtprod [definition, in mathcomp.ssreflect.order]
_ .-tupleprod (type_scope) [notation, in mathcomp.ssreflect.order]
_ .-tupleprod[ _ ] (type_scope) [notation, in mathcomp.ssreflect.order]
Order.TupleProdOrder.finCDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.finDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.finLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.finPOrderType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.finType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.join [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.joinA [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.joinC [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.joinEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.joinIB [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.joinKI [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.latticeMixin [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.latticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.leEmeet [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.leEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.lex1 [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.le0x [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.ltEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.meet [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetA [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetC [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetKU [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetUl [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.porderMixin [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.porderType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.sub [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.subEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.subKI [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.tbDistrLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.tbLatticeType [definition, in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_compl [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_sub [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_join [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_meet [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.topEtprod [lemma, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.Basics [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.Basics.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.BLattice [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.BLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.BLattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.CBDistrLattice [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.CBDistrLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.CBDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.CTBDistrLattice [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.CTBDistrLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.CTBDistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.DistrLattice [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.DistrLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.DistrLattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.Lattice [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.Lattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.Lattice.T [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.POrder [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.TBLattice [section, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.TBLattice.n [variable, in mathcomp.ssreflect.order]
Order.TupleProdOrder.TupleProdOrder.TBLattice.T [variable, in mathcomp.ssreflect.order]
_ .-tuple (type_scope) [notation, in mathcomp.ssreflect.order]
Order.TupleProdOrder.type [definition, in mathcomp.ssreflect.order]
Order.val_enum_ord [lemma, in mathcomp.ssreflect.order]
order1 [lemma, in mathcomp.fingroup.fingroup]
Ordinal [constructor, in mathcomp.ssreflect.fintype]
ordinal [inductive, in mathcomp.ssreflect.fintype]
OrdinalEnum [section, in mathcomp.ssreflect.fintype]
OrdinalEnum.n [variable, in mathcomp.ssreflect.fintype]
OrdinalPos [section, in mathcomp.ssreflect.fintype]
OrdinalPos.n' [variable, in mathcomp.ssreflect.fintype]
OrdinalSub [section, in mathcomp.ssreflect.fintype]
OrdinalSub.n [variable, in mathcomp.ssreflect.fintype]
ordinal_subFinType [definition, in mathcomp.ssreflect.fintype]
ordinal_finType [definition, in mathcomp.ssreflect.fintype]
ordinal_finMixin [definition, in mathcomp.ssreflect.fintype]
ordinal_subCountType [definition, in mathcomp.ssreflect.fintype]
ordinal_countType [definition, in mathcomp.ssreflect.fintype]
ordinal_countMixin [definition, in mathcomp.ssreflect.fintype]
ordinal_choiceType [definition, in mathcomp.ssreflect.fintype]
ordinal_choiceMixin [definition, in mathcomp.ssreflect.fintype]
ordinal_eqType [definition, in mathcomp.ssreflect.fintype]
ordinal_eqMixin [definition, in mathcomp.ssreflect.fintype]
ordinal_subType [definition, in mathcomp.ssreflect.fintype]
ordS [definition, in mathcomp.ssreflect.fintype]
ordSK [lemma, in mathcomp.ssreflect.fintype]
ordS_inj [lemma, in mathcomp.ssreflect.fintype]
ordS_bij [lemma, in mathcomp.ssreflect.fintype]
ordS_subproof [lemma, in mathcomp.ssreflect.fintype]
ord_tuple [definition, in mathcomp.ssreflect.tuple]
ord_enum4 [lemma, in mathcomp.solvable.burnside_app]
ord_max [definition, in mathcomp.ssreflect.fintype]
ord_pred_inj [lemma, in mathcomp.ssreflect.fintype]
ord_pred_bij [lemma, in mathcomp.ssreflect.fintype]
ord_predK [lemma, in mathcomp.ssreflect.fintype]
ord_pred [definition, in mathcomp.ssreflect.fintype]
ord_pred_subproof [lemma, in mathcomp.ssreflect.fintype]
ord_enum_uniq [lemma, in mathcomp.ssreflect.fintype]
ord_enum [definition, in mathcomp.ssreflect.fintype]
ord_inj [lemma, in mathcomp.ssreflect.fintype]
ord0 [definition, in mathcomp.ssreflect.fintype]
ord1 [lemma, in mathcomp.algebra.zmodp]
ord1 [lemma, in mathcomp.ssreflect.fintype]
ord:779 [binder, in mathcomp.ssreflect.fintype]
ord:788 [binder, in mathcomp.ssreflect.fintype]
ord:798 [binder, in mathcomp.ssreflect.fintype]
ord:810 [binder, in mathcomp.ssreflect.fintype]
orPP [lemma, in mathcomp.ssreflect.ssrbool]
orthogonal [definition, in mathcomp.character.classfun]
OrthogonalityRelations [section, in mathcomp.character.character]
OrthogonalityRelations.A [variable, in mathcomp.character.character]
OrthogonalityRelations.aT [variable, in mathcomp.character.character]
OrthogonalityRelations.G [variable, in mathcomp.character.character]
OrthogonalityRelations.gT [variable, in mathcomp.character.character]
OrthogonalityRelations.uX [variable, in mathcomp.character.character]
OrthogonalityRelations.XX'_1 [variable, in mathcomp.character.character]
OrthogonalityRelations.X' [variable, in mathcomp.character.character]
orthogonalP [lemma, in mathcomp.character.classfun]
orthogonal_span [lemma, in mathcomp.character.vcharacter]
orthogonal_free [lemma, in mathcomp.character.classfun]
orthogonal_oppl [lemma, in mathcomp.character.classfun]
orthogonal_oppr [lemma, in mathcomp.character.classfun]
orthogonal_split [lemma, in mathcomp.character.classfun]
orthogonal_catr [lemma, in mathcomp.character.classfun]
orthogonal_catl [lemma, in mathcomp.character.classfun]
orthogonal_sym [lemma, in mathcomp.character.classfun]
orthogonal_cons [lemma, in mathcomp.character.classfun]
orthonormal [definition, in mathcomp.character.classfun]
orthonormalE [lemma, in mathcomp.character.classfun]
orthonormalP [lemma, in mathcomp.character.classfun]
orthonormal_span [lemma, in mathcomp.character.vcharacter]
orthonormal_free [lemma, in mathcomp.character.classfun]
orthonormal_cat [lemma, in mathcomp.character.classfun]
orthonormal_orthogonal [lemma, in mathcomp.character.classfun]
orthonormal_not0 [lemma, in mathcomp.character.classfun]
orthonormal2P [lemma, in mathcomp.character.classfun]
orthoP [lemma, in mathcomp.character.classfun]
orthoPl [lemma, in mathcomp.character.classfun]
orthoPr [lemma, in mathcomp.character.classfun]
ortho_rec [definition, in mathcomp.character.classfun]
OtherEncodings [section, in mathcomp.ssreflect.choice]
OtherEncodings.T [variable, in mathcomp.ssreflect.choice]
OtherEncodings.T1 [variable, in mathcomp.ssreflect.choice]
OtherEncodings.T2 [variable, in mathcomp.ssreflect.choice]
out_perm [lemma, in mathcomp.fingroup.perm]
out_Aut [lemma, in mathcomp.fingroup.automorphism]

---

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

_

other

(79846 entries)

Notation 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

_

other

(1818 entries)

Binder 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

_

other

(48657 entries)

Module 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

_

other

(383 entries)

Variable 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

_

other

(4212 entries)

Library 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

_

other

(93 entries)

Lemma 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

_

other

(14712 entries)

Constructor 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

_

other

(223 entries)

Axiom 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

_

other

(45 entries)

Inductive 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

_

other

(132 entries)

Projection 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

_

other

(452 entries)

Section 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

_

other

(1429 entries)

Abbreviation 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

_

other

(1169 entries)

Definition 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

_

other

(6273 entries)

Record 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

_

other

(248 entries)