| 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 | (54001 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 | (1931 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 | (1658 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 | (7199 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 | (97 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 | (15214 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 | (75 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 | (224 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 | (2371 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 | (2266 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 | (732 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 | (21455 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 | (647 entries) |
O (lemma)
oACE [in mathcomp.ssreflect.bigop]oddB [in mathcomp.ssreflect.ssrnat]
oddb [in mathcomp.ssreflect.ssrnat]
oddD [in mathcomp.ssreflect.ssrnat]
oddM [in mathcomp.ssreflect.ssrnat]
oddN [in mathcomp.ssreflect.ssrnat]
oddS [in mathcomp.ssreflect.ssrnat]
oddSg [in mathcomp.solvable.pgroup]
oddX [in mathcomp.ssreflect.ssrnat]
odd_lift_perm [in mathcomp.fingroup.perm]
odd_permJ [in mathcomp.fingroup.perm]
odd_permV [in mathcomp.fingroup.perm]
odd_permM [in mathcomp.fingroup.perm]
odd_perm_prod [in mathcomp.fingroup.perm]
odd_tperm [in mathcomp.fingroup.perm]
odd_mul_tperm [in mathcomp.fingroup.perm]
odd_perm1 [in mathcomp.fingroup.perm]
odd_mod [in mathcomp.ssreflect.div]
odd_gt2 [in mathcomp.ssreflect.ssrnat]
odd_gt0 [in mathcomp.ssreflect.ssrnat]
odd_ltn [in mathcomp.ssreflect.ssrnat]
odd_geq [in mathcomp.ssreflect.ssrnat]
odd_uphalfK [in mathcomp.ssreflect.ssrnat]
odd_halfK [in mathcomp.ssreflect.ssrnat]
odd_double_half [in mathcomp.ssreflect.ssrnat]
odd_double [in mathcomp.ssreflect.ssrnat]
odd_pgroup_odd [in mathcomp.solvable.pgroup]
odd_2'nat [in mathcomp.ssreflect.prime]
odd_prime_gt2 [in mathcomp.ssreflect.prime]
odd_pgroup_rank1_cyclic [in mathcomp.solvable.extremal]
odd_not_extremal2 [in mathcomp.solvable.extremal]
odd_polyMX [in mathcomp.algebra.poly]
odd_poly_is_linear [in mathcomp.algebra.poly]
odd_polyZ [in mathcomp.algebra.poly]
odd_polyD [in mathcomp.algebra.poly]
odd_polyC [in mathcomp.algebra.poly]
odd_polyE [in mathcomp.algebra.poly]
of_irrK [in mathcomp.character.vcharacter]
OhmE [in mathcomp.solvable.abelian]
OhmEabelian [in mathcomp.solvable.abelian]
OhmJ [in mathcomp.solvable.abelian]
OhmPredP [in mathcomp.solvable.abelian]
OhmS [in mathcomp.solvable.abelian]
Ohm_Mho_homocyclic [in mathcomp.solvable.abelian]
Ohm_leq [in mathcomp.solvable.abelian]
Ohm_normal [in mathcomp.solvable.abelian]
Ohm_char [in mathcomp.solvable.abelian]
Ohm_dprod [in mathcomp.solvable.abelian]
Ohm_p_cycle [in mathcomp.solvable.abelian]
Ohm_cont [in mathcomp.solvable.abelian]
Ohm_id [in mathcomp.solvable.abelian]
Ohm_sub [in mathcomp.solvable.abelian]
Ohm0 [in mathcomp.solvable.abelian]
Ohm1 [in mathcomp.solvable.abelian]
Ohm1Eexponent [in mathcomp.solvable.abelian]
Ohm1Eprime [in mathcomp.solvable.abelian]
Ohm1_homocyclicP [in mathcomp.solvable.abelian]
Ohm1_cyclic_pgroup_prime [in mathcomp.solvable.abelian]
Ohm1_cent_max [in mathcomp.solvable.abelian]
Ohm1_eq1 [in mathcomp.solvable.abelian]
Ohm1_id [in mathcomp.solvable.abelian]
Ohm1_abelem [in mathcomp.solvable.abelian]
Ohm1_extraspecial_odd [in mathcomp.solvable.extraspecial]
Ohm1_cent_max_normal_abelem [in mathcomp.solvable.maximal]
Ohm1_stab_Ohm1_SCN_series [in mathcomp.solvable.maximal]
omapK [in mathcomp.ssreflect.ssrfun]
omap_id [in mathcomp.ssreflect.ssrfun]
oneg_ffun [in mathcomp.fingroup.gproduct]
on_card_preimset [in mathcomp.ssreflect.finset]
oopA_subdef [in mathcomp.ssreflect.bigop]
oopC_subdef [in mathcomp.ssreflect.bigop]
oopx1_subdef [in mathcomp.ssreflect.bigop]
oop1x_subdef [in mathcomp.ssreflect.bigop]
opair_of_sumK [in mathcomp.ssreflect.choice]
oppmx_key [in mathcomp.algebra.matrix]
oppq_frac [in mathcomp.algebra.rat]
oppr_itvcc [in mathcomp.algebra.interval]
oppr_itvoc [in mathcomp.algebra.interval]
oppr_itvco [in mathcomp.algebra.interval]
oppr_itvoo [in mathcomp.algebra.interval]
oppr_itv [in mathcomp.algebra.interval]
opp_block_mx [in mathcomp.algebra.matrix]
opp_col_mx [in mathcomp.algebra.matrix]
opp_row_mx [in mathcomp.algebra.matrix]
opp_isometry [in mathcomp.character.classfun]
opp_lfunE [in mathcomp.algebra.vector]
opp_poly_key [in mathcomp.algebra.poly]
option_enumP [in mathcomp.ssreflect.fintype]
opt_eqP [in mathcomp.ssreflect.eqtype]
op_Wedderburn_id [in mathcomp.character.mxrepresentation]
orbitE [in mathcomp.fingroup.action]
orbitE [in mathcomp.ssreflect.fingraph]
orbitJ [in mathcomp.fingroup.action]
orbitJs [in mathcomp.fingroup.action]
orbitP [in mathcomp.fingroup.action]
orbitPcycle [in mathcomp.ssreflect.fingraph]
orbitR [in mathcomp.fingroup.action]
orbitRs [in mathcomp.fingroup.action]
orbit_morphim_actperm [in mathcomp.fingroup.action]
orbit_conjsg [in mathcomp.fingroup.action]
orbit_rcoset [in mathcomp.fingroup.action]
orbit_lcoset [in mathcomp.fingroup.action]
orbit_inv [in mathcomp.fingroup.action]
orbit_eq_mem [in mathcomp.fingroup.action]
orbit_actr [in mathcomp.fingroup.action]
orbit_act [in mathcomp.fingroup.action]
orbit_transl [in mathcomp.fingroup.action]
orbit_eqP [in mathcomp.fingroup.action]
orbit_trans [in mathcomp.fingroup.action]
orbit_sym [in mathcomp.fingroup.action]
orbit_stabilizer [in mathcomp.fingroup.action]
orbit_transversalP [in mathcomp.fingroup.action]
orbit_partition [in mathcomp.fingroup.action]
orbit_conjsg_in [in mathcomp.fingroup.action]
orbit_rcoset_in [in mathcomp.fingroup.action]
orbit_lcoset_in [in mathcomp.fingroup.action]
orbit_inv_in [in mathcomp.fingroup.action]
orbit_actr_in [in mathcomp.fingroup.action]
orbit_act_in [in mathcomp.fingroup.action]
orbit_in_transl [in mathcomp.fingroup.action]
orbit_in_eqP [in mathcomp.fingroup.action]
orbit_in_trans [in mathcomp.fingroup.action]
orbit_in_sym [in mathcomp.fingroup.action]
orbit_refl [in mathcomp.fingroup.action]
orbit_id [in mathcomp.ssreflect.fingraph]
orbit_rot_cycle [in mathcomp.ssreflect.fingraph]
orbit_uniq [in mathcomp.ssreflect.fingraph]
orbit1P [in mathcomp.fingroup.action]
orderE [in mathcomp.fingroup.fingroup]
orderJ [in mathcomp.fingroup.fingroup]
orderM [in mathcomp.solvable.cyclic]
orderPcycle [in mathcomp.ssreflect.fingraph]
orderSpred [in mathcomp.ssreflect.fingraph]
orderV [in mathcomp.fingroup.fingroup]
orderXdiv [in mathcomp.solvable.cyclic]
orderXdvd [in mathcomp.solvable.cyclic]
orderXexp [in mathcomp.solvable.cyclic]
orderXgcd [in mathcomp.solvable.cyclic]
orderXpfactor [in mathcomp.solvable.cyclic]
orderXpnat [in mathcomp.solvable.cyclic]
orderXprime [in mathcomp.solvable.cyclic]
order_Zp1 [in mathcomp.algebra.zmodp]
order_gt1 [in mathcomp.fingroup.fingroup]
order_eq1 [in mathcomp.fingroup.fingroup]
order_gt0 [in mathcomp.fingroup.fingroup]
order_constt [in mathcomp.solvable.pgroup]
order_path_min [in mathcomp.ssreflect.path]
order_path_min_in [in mathcomp.ssreflect.path]
order_primeChar [in mathcomp.field.finfield]
order_injm [in mathcomp.fingroup.morphism]
order_set_finv [in mathcomp.ssreflect.fingraph]
order_finv [in mathcomp.ssreflect.fingraph]
order_id [in mathcomp.ssreflect.fingraph]
order_id_cycle [in mathcomp.ssreflect.fingraph]
order_cycle [in mathcomp.ssreflect.fingraph]
order_le_cycle [in mathcomp.ssreflect.fingraph]
order_gt0 [in mathcomp.ssreflect.fingraph]
order_inj_cyclic [in mathcomp.solvable.cyclic]
order_dvdG [in mathcomp.solvable.cyclic]
order_inf [in mathcomp.solvable.cyclic]
order_dvdn [in mathcomp.solvable.cyclic]
Order.BDistrLatticeTheory.disjoint_lexUr [in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.disjoint_lexUl [in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.joins_disjoint [in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.leU2E [in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.leU2l_le [in mathcomp.ssreflect.order]
Order.BDistrLatticeTheory.leU2r_le [in mathcomp.ssreflect.order]
Order.BJoinTheory.joinsP [in mathcomp.ssreflect.order]
Order.BJoinTheory.joinsP_seq [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_seq [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_setU [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_le [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_min [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_sup [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_min_seq [in mathcomp.ssreflect.order]
Order.BJoinTheory.joins_sup_seq [in mathcomp.ssreflect.order]
Order.BJoinTheory.joinx0 [in mathcomp.ssreflect.order]
Order.BJoinTheory.join_eq0 [in mathcomp.ssreflect.order]
Order.BJoinTheory.join0x [in mathcomp.ssreflect.order]
Order.BJoinTheory.le_joins [in mathcomp.ssreflect.order]
Order.BLatticeMorphismTheory.comp_is_bottom_morphism [in mathcomp.ssreflect.order]
Order.BLatticeMorphismTheory.idfun_is_bottom_morphism [in mathcomp.ssreflect.order]
Order.BLatticeMorphismTheory.omorph0 [in mathcomp.ssreflect.order]
Order.BMeetTheory.meetx0 [in mathcomp.ssreflect.order]
Order.BMeetTheory.meet0x [in mathcomp.ssreflect.order]
Order.BoolOrder.andbE [in mathcomp.ssreflect.order]
Order.BoolOrder.andEbool [in mathcomp.ssreflect.order]
Order.BoolOrder.anti [in mathcomp.ssreflect.order]
Order.BoolOrder.bool_display [in mathcomp.ssreflect.order]
Order.BoolOrder.complEbool [in mathcomp.ssreflect.order]
Order.BoolOrder.leEbool [in mathcomp.ssreflect.order]
Order.BoolOrder.ltEbool [in mathcomp.ssreflect.order]
Order.BoolOrder.ltn_def [in mathcomp.ssreflect.order]
Order.BoolOrder.orbE [in mathcomp.ssreflect.order]
Order.BoolOrder.orEbool [in mathcomp.ssreflect.order]
Order.BoolOrder.subEbool [in mathcomp.ssreflect.order]
Order.BPOrderTheory.lex0 [in mathcomp.ssreflect.order]
Order.BPOrderTheory.le0x [in mathcomp.ssreflect.order]
Order.BPOrderTheory.ltx0 [in mathcomp.ssreflect.order]
Order.BPOrderTheory.lt0x [in mathcomp.ssreflect.order]
Order.BPOrderTheory.posxP [in mathcomp.ssreflect.order]
Order.Builders_468.opredU [in mathcomp.ssreflect.order]
Order.Builders_468.opredI [in mathcomp.ssreflect.order]
Order.Builders_462.totalU [in mathcomp.ssreflect.order]
Order.Builders_415.val1 [in mathcomp.ssreflect.order]
Order.Builders_415.lex1 [in mathcomp.ssreflect.order]
Order.Builders_392.val0 [in mathcomp.ssreflect.order]
Order.Builders_392.le0x [in mathcomp.ssreflect.order]
Order.Builders_363.valU [in mathcomp.ssreflect.order]
Order.Builders_363.valI [in mathcomp.ssreflect.order]
Order.Builders_363.joinUKI [in mathcomp.ssreflect.order]
Order.Builders_344.valD [in mathcomp.ssreflect.order]
Order.Builders_290.meetUl [in mathcomp.ssreflect.order]
Order.Builders_284.meet_eql [in mathcomp.ssreflect.order]
Order.Builders_284.meetKI [in mathcomp.ssreflect.order]
Order.Builders_284.joinKI [in mathcomp.ssreflect.order]
Order.Builders_284.joinA [in mathcomp.ssreflect.order]
Order.Builders_284.meetA [in mathcomp.ssreflect.order]
Order.Builders_284.joinC [in mathcomp.ssreflect.order]
Order.Builders_284.meetC [in mathcomp.ssreflect.order]
Order.Builders_245.totalT [in mathcomp.ssreflect.order]
Order.Builders_236.le_total [in mathcomp.ssreflect.order]
Order.Builders_236.le_trans [in mathcomp.ssreflect.order]
Order.Builders_236.le_anti [in mathcomp.ssreflect.order]
Order.Builders_236.join_def_le [in mathcomp.ssreflect.order]
Order.Builders_236.meet_def_le [in mathcomp.ssreflect.order]
Order.Builders_236.lt_def [in mathcomp.ssreflect.order]
Order.Builders_209.le_def [in mathcomp.ssreflect.order]
Order.Builders_209.meetxx [in mathcomp.ssreflect.order]
Order.Builders_209.meetUl [in mathcomp.ssreflect.order]
Order.Builders_209.meetKU [in mathcomp.ssreflect.order]
Order.Builders_209.joinKI [in mathcomp.ssreflect.order]
Order.Builders_209.joinA [in mathcomp.ssreflect.order]
Order.Builders_209.meetA [in mathcomp.ssreflect.order]
Order.Builders_209.joinC [in mathcomp.ssreflect.order]
Order.Builders_209.meetC [in mathcomp.ssreflect.order]
Order.Builders_209.joinE [in mathcomp.ssreflect.order]
Order.Builders_209.meetE [in mathcomp.ssreflect.order]
Order.Builders_209.le_refl [in mathcomp.ssreflect.order]
Order.Builders_200.leEmeet [in mathcomp.ssreflect.order]
Order.Builders_200.meetKU [in mathcomp.ssreflect.order]
Order.Builders_200.joinKI [in mathcomp.ssreflect.order]
Order.Builders_200.joinA [in mathcomp.ssreflect.order]
Order.Builders_200.meetA [in mathcomp.ssreflect.order]
Order.Builders_200.joinC [in mathcomp.ssreflect.order]
Order.Builders_200.meetC [in mathcomp.ssreflect.order]
Order.Builders_200.leP [in mathcomp.ssreflect.order]
Order.Builders_200.ltgtP [in mathcomp.ssreflect.order]
Order.Builders_193.meetUl [in mathcomp.ssreflect.order]
Order.Builders_183.complEcodiff [in mathcomp.ssreflect.order]
Order.Builders_183.complEdiff [in mathcomp.ssreflect.order]
Order.Builders_183.codiffErcompl [in mathcomp.ssreflect.order]
Order.Builders_183.joinIB [in mathcomp.ssreflect.order]
Order.Builders_183.diffKI [in mathcomp.ssreflect.order]
Order.Builders_176.complEdiff [in mathcomp.ssreflect.order]
Order.Builders_169.complEcodiff [in mathcomp.ssreflect.order]
Order.Builders_162.codiffErcompl [in mathcomp.ssreflect.order]
Order.Builders_162.rcomplPjoin [in mathcomp.ssreflect.order]
Order.Builders_162.rcomplPmeet [in mathcomp.ssreflect.order]
Order.Builders_155.diffErcompl [in mathcomp.ssreflect.order]
Order.Builders_155.rcomplPjoin [in mathcomp.ssreflect.order]
Order.Builders_155.rcomplPmeet [in mathcomp.ssreflect.order]
Order.Builders_146.le_trans [in mathcomp.ssreflect.order]
Order.Builders_146.le_anti [in mathcomp.ssreflect.order]
Order.Builders_146.le_refl [in mathcomp.ssreflect.order]
Order.Builders_127.leUx [in mathcomp.ssreflect.order]
Order.Builders_127.joinxx [in mathcomp.ssreflect.order]
Order.Builders_127.lexI [in mathcomp.ssreflect.order]
Order.Builders_127.meetxx [in mathcomp.ssreflect.order]
Order.Builders_127.leEjoin [in mathcomp.ssreflect.order]
Order.Builders_115.leUx [in mathcomp.ssreflect.order]
Order.Builders_115.joinxx [in mathcomp.ssreflect.order]
Order.Builders_110.lexI [in mathcomp.ssreflect.order]
Order.Builders_110.meetxx [in mathcomp.ssreflect.order]
Order.Builders_90.ge_anti [in mathcomp.ssreflect.order]
Order.Builders_90.gt_def [in mathcomp.ssreflect.order]
Order.CancelPartial.anti [in mathcomp.ssreflect.order]
Order.CancelPartial.lt_def [in mathcomp.ssreflect.order]
Order.CancelPartial.refl [in mathcomp.ssreflect.order]
Order.CancelPartial.trans [in mathcomp.ssreflect.order]
Order.cardE [in mathcomp.ssreflect.order]
Order.cardT [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffBx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffErcompl [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffIK [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffIx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffKI [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffKU [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffUK [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffUx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffxB [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffxI [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffxU [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffxx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diffx0 [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diff_eq0 [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.diff0x [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_diffr [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_diffl [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_leC [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.disj_le [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.eq_diff [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBI [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBIC [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBK [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBKC [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinBx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinIB [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinIBC [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.joinxB [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBKU [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBl [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBLR [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBr [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBRL [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBUK [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leBx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.leB2 [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.lt0B [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetBI [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetBx [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetIB [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meetxB [in mathcomp.ssreflect.order]
Order.CBDistrLatticeTheory.meet_eq0E_diff [in mathcomp.ssreflect.order]
Order.CDistrLatticeTheory.rcomplKI [in mathcomp.ssreflect.order]
Order.CDistrLatticeTheory.rcomplKU [in mathcomp.ssreflect.order]
Order.CDistrLatticeTheory.rcomplPjoin [in mathcomp.ssreflect.order]
Order.CDistrLatticeTheory.rcomplPmeet [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complB [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complEcodiff [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complEdiff [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complErcompl [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complI [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complK [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.complU [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl_meets [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl_joins [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl_inj [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl0 [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.compl1 [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.diffE [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.diff1x [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.disj_leC [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.joinCx [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.joinxC [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.leBC [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.leC [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.leCx [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.lexC [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.meetCx [in mathcomp.ssreflect.order]
Order.CTBDistrLatticeTheory.meetxC [in mathcomp.ssreflect.order]
Order.CTDistrLatticeTheory.codiffErcompl [in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.joinIl [in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.joinIr [in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.meetUl [in mathcomp.ssreflect.order]
Order.DistrLatticeTheory.meetUr [in mathcomp.ssreflect.order]
Order.DualOrder.botEdual [in mathcomp.ssreflect.order]
Order.DualOrder.joinEdual [in mathcomp.ssreflect.order]
Order.DualOrder.leEdual [in mathcomp.ssreflect.order]
Order.DualOrder.ltEdual [in mathcomp.ssreflect.order]
Order.DualOrder.meetEdual [in mathcomp.ssreflect.order]
Order.DualOrder.topEdual [in mathcomp.ssreflect.order]
Order.dvd_display [in mathcomp.ssreflect.order]
Order.enumT [in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_bij [in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_bij [in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_in_inj [in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_bij_in [in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_inj [in mathcomp.ssreflect.order]
Order.EnumVal.enum_rank_inj [in mathcomp.ssreflect.order]
Order.EnumVal.enum_valK [in mathcomp.ssreflect.order]
Order.EnumVal.enum_valK_in [in mathcomp.ssreflect.order]
Order.EnumVal.enum_rankK [in mathcomp.ssreflect.order]
Order.EnumVal.enum_rankK_in [in mathcomp.ssreflect.order]
Order.EnumVal.enum_val_nth [in mathcomp.ssreflect.order]
Order.EnumVal.enum_valP [in mathcomp.ssreflect.order]
Order.EnumVal.eq_enum_rank_in [in mathcomp.ssreflect.order]
Order.EnumVal.le_enum_rank [in mathcomp.ssreflect.order]
Order.EnumVal.le_enum_rank_in [in mathcomp.ssreflect.order]
Order.EnumVal.le_enum_val [in mathcomp.ssreflect.order]
Order.EnumVal.nth_enum_rank [in mathcomp.ssreflect.order]
Order.EnumVal.nth_enum_rank_in [in mathcomp.ssreflect.order]
Order.enum_ord [in mathcomp.ssreflect.order]
Order.enum_set1 [in mathcomp.ssreflect.order]
Order.enum_setT [in mathcomp.ssreflect.order]
Order.enum_set0 [in mathcomp.ssreflect.order]
Order.enum_uniq [in mathcomp.ssreflect.order]
Order.enum0 [in mathcomp.ssreflect.order]
Order.enum1 [in mathcomp.ssreflect.order]
Order.eq_cardT [in mathcomp.ssreflect.order]
Order.eq_enum [in mathcomp.ssreflect.order]
Order.index_enum_ord [in mathcomp.ssreflect.order]
Order.JoinTheory.eq_joinr [in mathcomp.ssreflect.order]
Order.JoinTheory.eq_joinl [in mathcomp.ssreflect.order]
Order.JoinTheory.joinA [in mathcomp.ssreflect.order]
Order.JoinTheory.joinAC [in mathcomp.ssreflect.order]
Order.JoinTheory.joinACA [in mathcomp.ssreflect.order]
Order.JoinTheory.joinC [in mathcomp.ssreflect.order]
Order.JoinTheory.joinCA [in mathcomp.ssreflect.order]
Order.JoinTheory.joinKU [in mathcomp.ssreflect.order]
Order.JoinTheory.joinKUC [in mathcomp.ssreflect.order]
Order.JoinTheory.joinUK [in mathcomp.ssreflect.order]
Order.JoinTheory.joinUKC [in mathcomp.ssreflect.order]
Order.JoinTheory.joinxx [in mathcomp.ssreflect.order]
Order.JoinTheory.join_r [in mathcomp.ssreflect.order]
Order.JoinTheory.join_l [in mathcomp.ssreflect.order]
Order.JoinTheory.join_idPr [in mathcomp.ssreflect.order]
Order.JoinTheory.join_idPl [in mathcomp.ssreflect.order]
Order.JoinTheory.leEjoin [in mathcomp.ssreflect.order]
Order.JoinTheory.leUidl [in mathcomp.ssreflect.order]
Order.JoinTheory.leUidr [in mathcomp.ssreflect.order]
Order.JoinTheory.leUl [in mathcomp.ssreflect.order]
Order.JoinTheory.leUr [in mathcomp.ssreflect.order]
Order.JoinTheory.leUx [in mathcomp.ssreflect.order]
Order.JoinTheory.leU2 [in mathcomp.ssreflect.order]
Order.JoinTheory.lexUl [in mathcomp.ssreflect.order]
Order.JoinTheory.lexUr [in mathcomp.ssreflect.order]
Order.JoinTheory.lexU2 [in mathcomp.ssreflect.order]
Order.LatticeMorphismTheory.comp_is_join_morphism [in mathcomp.ssreflect.order]
Order.LatticeMorphismTheory.comp_is_meet_morphism [in mathcomp.ssreflect.order]
Order.LatticeMorphismTheory.idfun_is_join_morphism [in mathcomp.ssreflect.order]
Order.LatticeMorphismTheory.idfun_is_meet_morphism [in mathcomp.ssreflect.order]
Order.LatticeMorphismTheory.omorphI [in mathcomp.ssreflect.order]
Order.LatticeMorphismTheory.omorphU [in mathcomp.ssreflect.order]
Order.LatticePred.opredI [in mathcomp.ssreflect.order]
Order.LatticePred.opredU [in mathcomp.ssreflect.order]
Order.LatticePred.opred_meets [in mathcomp.ssreflect.order]
Order.LatticePred.opred_joins [in mathcomp.ssreflect.order]
Order.LatticePred.opred0 [in mathcomp.ssreflect.order]
Order.LatticePred.opred1 [in mathcomp.ssreflect.order]
Order.LatticeTheory.joinIK [in mathcomp.ssreflect.order]
Order.LatticeTheory.joinIKC [in mathcomp.ssreflect.order]
Order.LatticeTheory.joinKI [in mathcomp.ssreflect.order]
Order.LatticeTheory.joinKIC [in mathcomp.ssreflect.order]
Order.LatticeTheory.lcomparableP [in mathcomp.ssreflect.order]
Order.LatticeTheory.lcomparable_ltP [in mathcomp.ssreflect.order]
Order.LatticeTheory.lcomparable_leP [in mathcomp.ssreflect.order]
Order.LatticeTheory.lcomparable_ltgtP [in mathcomp.ssreflect.order]
Order.LatticeTheory.meetKU [in mathcomp.ssreflect.order]
Order.LatticeTheory.meetKUC [in mathcomp.ssreflect.order]
Order.LatticeTheory.meetUK [in mathcomp.ssreflect.order]
Order.LatticeTheory.meetUKC [in mathcomp.ssreflect.order]
Order.lexi_display [in mathcomp.ssreflect.order]
Order.MeetTheory.eq_meetr [in mathcomp.ssreflect.order]
Order.MeetTheory.eq_meetl [in mathcomp.ssreflect.order]
Order.MeetTheory.leEmeet [in mathcomp.ssreflect.order]
Order.MeetTheory.leIidl [in mathcomp.ssreflect.order]
Order.MeetTheory.leIidr [in mathcomp.ssreflect.order]
Order.MeetTheory.leIl [in mathcomp.ssreflect.order]
Order.MeetTheory.leIr [in mathcomp.ssreflect.order]
Order.MeetTheory.leIxl [in mathcomp.ssreflect.order]
Order.MeetTheory.leIxr [in mathcomp.ssreflect.order]
Order.MeetTheory.leIx2 [in mathcomp.ssreflect.order]
Order.MeetTheory.leI2 [in mathcomp.ssreflect.order]
Order.MeetTheory.lexI [in mathcomp.ssreflect.order]
Order.MeetTheory.meetA [in mathcomp.ssreflect.order]
Order.MeetTheory.meetAC [in mathcomp.ssreflect.order]
Order.MeetTheory.meetACA [in mathcomp.ssreflect.order]
Order.MeetTheory.meetC [in mathcomp.ssreflect.order]
Order.MeetTheory.meetCA [in mathcomp.ssreflect.order]
Order.MeetTheory.meetIK [in mathcomp.ssreflect.order]
Order.MeetTheory.meetIKC [in mathcomp.ssreflect.order]
Order.MeetTheory.meetKI [in mathcomp.ssreflect.order]
Order.MeetTheory.meetKIC [in mathcomp.ssreflect.order]
Order.MeetTheory.meetxx [in mathcomp.ssreflect.order]
Order.MeetTheory.meet_r [in mathcomp.ssreflect.order]
Order.MeetTheory.meet_l [in mathcomp.ssreflect.order]
Order.MeetTheory.meet_idPr [in mathcomp.ssreflect.order]
Order.MeetTheory.meet_idPl [in mathcomp.ssreflect.order]
Order.mem_enum [in mathcomp.ssreflect.order]
Order.mono_unique [in mathcomp.ssreflect.order]
Order.mono_sorted_enum [in mathcomp.ssreflect.order]
Order.NatDvd.dvdE [in mathcomp.ssreflect.order]
Order.NatDvd.gcdE [in mathcomp.ssreflect.order]
Order.NatDvd.joinKI [in mathcomp.ssreflect.order]
Order.NatDvd.lcmE [in mathcomp.ssreflect.order]
Order.NatDvd.lcmnn [in mathcomp.ssreflect.order]
Order.NatDvd.le_def [in mathcomp.ssreflect.order]
Order.NatDvd.meetKU [in mathcomp.ssreflect.order]
Order.NatDvd.meetUl [in mathcomp.ssreflect.order]
Order.NatDvd.nat0E [in mathcomp.ssreflect.order]
Order.NatDvd.nat1E [in mathcomp.ssreflect.order]
Order.NatDvd.sdvdE [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.decnP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.decn_inP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.homo_ltn_lt [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.homo_ltn_lt_in [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.incnP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.incn_inP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nhomo_ltn_lt [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nhomo_ltn_lt_in [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nondecnP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nondecn_inP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nonincnP [in mathcomp.ssreflect.order]
Order.NatMonotonyTheory.nonincn_inP [in mathcomp.ssreflect.order]
Order.NatOrder.botEnat [in mathcomp.ssreflect.order]
Order.NatOrder.leEnat [in mathcomp.ssreflect.order]
Order.NatOrder.ltEnat [in mathcomp.ssreflect.order]
Order.NatOrder.ltn_def [in mathcomp.ssreflect.order]
Order.NatOrder.maxEnat [in mathcomp.ssreflect.order]
Order.NatOrder.minEnat [in mathcomp.ssreflect.order]
Order.NatOrder.nat_display [in mathcomp.ssreflect.order]
Order.nth_ord_enum [in mathcomp.ssreflect.order]
Order.nth_enum_ord [in mathcomp.ssreflect.order]
Order.OrderMorphismTheory.comp_is_nondecreasing [in mathcomp.ssreflect.order]
Order.OrderMorphismTheory.idfun_is_nondecreasing [in mathcomp.ssreflect.order]
Order.OrderMorphismTheory.omorph_lt [in mathcomp.ssreflect.order]
Order.OrderMorphismTheory.omorph_le [in mathcomp.ssreflect.order]
Order.OrdinalOrder.botEord [in mathcomp.ssreflect.order]
Order.OrdinalOrder.leEord [in mathcomp.ssreflect.order]
Order.OrdinalOrder.ltEord [in mathcomp.ssreflect.order]
Order.OrdinalOrder.ord_display [in mathcomp.ssreflect.order]
Order.OrdinalOrder.topEord [in mathcomp.ssreflect.order]
Order.POrderTheory.bigmax_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.bigmax_le [in mathcomp.ssreflect.order]
Order.POrderTheory.comparableP [in mathcomp.ssreflect.order]
Order.POrderTheory.comparablexx [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_lt_le [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_le_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_le [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_ltn_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_ltn_le [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_leq_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_leq_le [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraFlt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraFle [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_not_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contra_not_le [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraNlt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraNle [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraPlt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraPle [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraTlt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_contraTle [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_bigr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_bigl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_arg_maxP [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_arg_minP [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_min_maxr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_max_minr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxACA [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minACA [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxCA [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minCA [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxAC [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minAC [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_min_maxl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_max_minl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxA [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minA [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_maxl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_maxr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_minl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteif_minr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lteifNE [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxKx [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxxK [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minKx [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minxK [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_gt_max [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lt_max [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ge_max [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_le_max [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_gt_min [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_lt_min [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ge_min [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_le_min [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_max_idPl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_min_idPr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_eq_maxl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_eq_minr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxC [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minC [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minr [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minl [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxEge [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minEge [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_maxEgt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_minEgt [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_sym [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ltP [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_leP [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ltgtP [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_ltNge [in mathcomp.ssreflect.order]
Order.POrderTheory.comparable_leNgt [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_lt_ltn [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_lt_leq [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_le_ltn [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_le_leq [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_ltF [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_leF [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_lt_not [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_le_not [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_ltN [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_leN [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_ltT [in mathcomp.ssreflect.order]
Order.POrderTheory.contra_leT [in mathcomp.ssreflect.order]
Order.POrderTheory.count_lt_le_mem [in mathcomp.ssreflect.order]
Order.POrderTheory.count_le_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.count_lt_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.dec_inj_in [in mathcomp.ssreflect.order]
Order.POrderTheory.dec_inj [in mathcomp.ssreflect.order]
Order.POrderTheory.eqTleif [in mathcomp.ssreflect.order]
Order.POrderTheory.eq_maxr [in mathcomp.ssreflect.order]
Order.POrderTheory.eq_minl [in mathcomp.ssreflect.order]
Order.POrderTheory.eq_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.eq_le [in mathcomp.ssreflect.order]
Order.POrderTheory.filter_le_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.filter_lt_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.geE [in mathcomp.ssreflect.order]
Order.POrderTheory.ge_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.ge_comparable [in mathcomp.ssreflect.order]
Order.POrderTheory.ge_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.ge_anti [in mathcomp.ssreflect.order]
Order.POrderTheory.gtE [in mathcomp.ssreflect.order]
Order.POrderTheory.gt_comparable [in mathcomp.ssreflect.order]
Order.POrderTheory.gt_eqF [in mathcomp.ssreflect.order]
Order.POrderTheory.incomparable_ltF [in mathcomp.ssreflect.order]
Order.POrderTheory.incomparable_leF [in mathcomp.ssreflect.order]
Order.POrderTheory.incomparable_eqF [in mathcomp.ssreflect.order]
Order.POrderTheory.inc_inj_in [in mathcomp.ssreflect.order]
Order.POrderTheory.inc_inj [in mathcomp.ssreflect.order]
Order.POrderTheory.inj_nhomo_lt_in [in mathcomp.ssreflect.order]
Order.POrderTheory.inj_homo_lt_in [in mathcomp.ssreflect.order]
Order.POrderTheory.inj_nhomo_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.inj_homo_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.leifP [in mathcomp.ssreflect.order]
Order.POrderTheory.leif_eq [in mathcomp.ssreflect.order]
Order.POrderTheory.leif_le [in mathcomp.ssreflect.order]
Order.POrderTheory.leif_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.leif_refl [in mathcomp.ssreflect.order]
Order.POrderTheory.leW_nmono_in [in mathcomp.ssreflect.order]
Order.POrderTheory.leW_mono_in [in mathcomp.ssreflect.order]
Order.POrderTheory.leW_nmono [in mathcomp.ssreflect.order]
Order.POrderTheory.leW_mono [in mathcomp.ssreflect.order]
Order.POrderTheory.lexx [in mathcomp.ssreflect.order]
Order.POrderTheory.le_bigmin [in mathcomp.ssreflect.order]
Order.POrderTheory.le_comparable [in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_eq [in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_leq_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_ltn_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_filter [in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_mask [in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_filter [in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_mask [in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_pairwise [in mathcomp.ssreflect.order]
Order.POrderTheory.le_sorted_pairwise [in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_sortedE [in mathcomp.ssreflect.order]
Order.POrderTheory.le_path_min [in mathcomp.ssreflect.order]
Order.POrderTheory.le_lt_asym [in mathcomp.ssreflect.order]
Order.POrderTheory.le_gtF [in mathcomp.ssreflect.order]
Order.POrderTheory.le_lt_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.le_eqVlt [in mathcomp.ssreflect.order]
Order.POrderTheory.le_le_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.le_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.le_anti [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifF [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifN [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifNF [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifS [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifT [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifW [in mathcomp.ssreflect.order]
Order.POrderTheory.lteifxx [in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_imply [in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_andb [in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_orb [in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_anti [in mathcomp.ssreflect.order]
Order.POrderTheory.lteif_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.ltNleif [in mathcomp.ssreflect.order]
Order.POrderTheory.ltrW_lteif [in mathcomp.ssreflect.order]
Order.POrderTheory.ltW [in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_nhomo_in [in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_homo_in [in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_nhomo [in mathcomp.ssreflect.order]
Order.POrderTheory.ltW_homo [in mathcomp.ssreflect.order]
Order.POrderTheory.ltxx [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_bigmin [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_comparable [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_eq [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_uniq [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_ltn_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_leq_nth [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_filter [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_mask [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_filter [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_mask [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_uniq_le [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_pairwise [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_sorted_pairwise [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_sortedE [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_path_min [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_le_asym [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_leAnge [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_geF [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_asym [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_nsym [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_le_trans [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_eqF [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_neqAle [in mathcomp.ssreflect.order]
Order.POrderTheory.lt_def [in mathcomp.ssreflect.order]
Order.POrderTheory.maxEle [in mathcomp.ssreflect.order]
Order.POrderTheory.maxElt [in mathcomp.ssreflect.order]
Order.POrderTheory.maxxx [in mathcomp.ssreflect.order]
Order.POrderTheory.max_maxxK [in mathcomp.ssreflect.order]
Order.POrderTheory.max_maxKx [in mathcomp.ssreflect.order]
Order.POrderTheory.max_idPr [in mathcomp.ssreflect.order]
Order.POrderTheory.max_r [in mathcomp.ssreflect.order]
Order.POrderTheory.max_l [in mathcomp.ssreflect.order]
Order.POrderTheory.minEle [in mathcomp.ssreflect.order]
Order.POrderTheory.minElt [in mathcomp.ssreflect.order]
Order.POrderTheory.minxx [in mathcomp.ssreflect.order]
Order.POrderTheory.min_minxK [in mathcomp.ssreflect.order]
Order.POrderTheory.min_minKx [in mathcomp.ssreflect.order]
Order.POrderTheory.min_idPl [in mathcomp.ssreflect.order]
Order.POrderTheory.min_r [in mathcomp.ssreflect.order]
Order.POrderTheory.min_l [in mathcomp.ssreflect.order]
Order.POrderTheory.mono_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.mono_in_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.nmono_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.nmono_in_leif [in mathcomp.ssreflect.order]
Order.POrderTheory.nth_count_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.nth_count_le [in mathcomp.ssreflect.order]
Order.POrderTheory.sorted_filter_le [in mathcomp.ssreflect.order]
Order.POrderTheory.sorted_filter_lt [in mathcomp.ssreflect.order]
Order.POrderTheory.sort_lt_id [in mathcomp.ssreflect.order]
Order.POrderTheory.sort_le_id [in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_lt_sorted [in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_le_sorted [in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_lt_path [in mathcomp.ssreflect.order]
Order.POrderTheory.subseq_le_path [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.anti [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.botEprodlexi [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.leEprodlexi [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.lexi_pair [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.le0x [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ltEprodlexi [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.ltxi_pair [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.lt_def [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.refl [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.sub_prod_lexi [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.topEprodlexi [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.total [in mathcomp.ssreflect.order]
Order.ProdLexiOrder.trans [in mathcomp.ssreflect.order]
Order.ProdOrder.anti [in mathcomp.ssreflect.order]
Order.ProdOrder.botEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.codiffEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.complEdiff [in mathcomp.ssreflect.order]
Order.ProdOrder.complEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.diffEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.diffErcompl [in mathcomp.ssreflect.order]
Order.ProdOrder.joinEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.leEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.lexI [in mathcomp.ssreflect.order]
Order.ProdOrder.le_pair [in mathcomp.ssreflect.order]
Order.ProdOrder.le0x [in mathcomp.ssreflect.order]
Order.ProdOrder.ltEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.lt_pair [in mathcomp.ssreflect.order]
Order.ProdOrder.lt_def [in mathcomp.ssreflect.order]
Order.ProdOrder.meetEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.meetUl [in mathcomp.ssreflect.order]
Order.ProdOrder.rcomplEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.rcomplPmeet [in mathcomp.ssreflect.order]
Order.ProdOrder.refl [in mathcomp.ssreflect.order]
Order.ProdOrder.topEprod [in mathcomp.ssreflect.order]
Order.ProdOrder.trans [in mathcomp.ssreflect.order]
Order.prod_display_unit [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.anti [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.eqhead_ltxiE [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.eqhead_lexiE [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.leEseqlexi [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexis0 [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexi_lehead [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexi_cons [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lexi0s [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltEseqlexi [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxis0 [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxi_lehead [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxi_cons [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.ltxi0s [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.lt_def [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.neqhead_ltxiE [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.neqhead_lexiE [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.refl [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.sub_seqprod_lexi [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.total [in mathcomp.ssreflect.order]
Order.SeqLexiOrder.trans [in mathcomp.ssreflect.order]
Order.seqlexi_display [in mathcomp.ssreflect.order]
Order.SeqProdOrder.anti [in mathcomp.ssreflect.order]
Order.SeqProdOrder.botEseq [in mathcomp.ssreflect.order]
Order.SeqProdOrder.joinEseq [in mathcomp.ssreflect.order]
Order.SeqProdOrder.join_cons [in mathcomp.ssreflect.order]
Order.SeqProdOrder.leEseq [in mathcomp.ssreflect.order]
Order.SeqProdOrder.les0 [in mathcomp.ssreflect.order]
Order.SeqProdOrder.leUx [in mathcomp.ssreflect.order]
Order.SeqProdOrder.lexI [in mathcomp.ssreflect.order]
Order.SeqProdOrder.le_cons [in mathcomp.ssreflect.order]
Order.SeqProdOrder.le0s [in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetEseq [in mathcomp.ssreflect.order]
Order.SeqProdOrder.meetUl [in mathcomp.ssreflect.order]
Order.SeqProdOrder.meet_cons [in mathcomp.ssreflect.order]
Order.SeqProdOrder.refl [in mathcomp.ssreflect.order]
Order.SeqProdOrder.trans [in mathcomp.ssreflect.order]
Order.seqprod_display [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.botEsubset [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.complEsubset [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.joinEsubset [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.leEsubset [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.le_def [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.meetEsubset [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setIDv [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setKIC [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setKUC [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.setTDsym [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.subEsubset [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.subset_display [in mathcomp.ssreflect.order]
Order.SetSubsetOrder.topEsubset [in mathcomp.ssreflect.order]
Order.set_enum [in mathcomp.ssreflect.order]
Order.SigmaOrder.anti [in mathcomp.ssreflect.order]
Order.SigmaOrder.botEsig [in mathcomp.ssreflect.order]
Order.SigmaOrder.leEsig [in mathcomp.ssreflect.order]
Order.SigmaOrder.lex1 [in mathcomp.ssreflect.order]
Order.SigmaOrder.le_Taggedr [in mathcomp.ssreflect.order]
Order.SigmaOrder.le_Taggedl [in mathcomp.ssreflect.order]
Order.SigmaOrder.le0x [in mathcomp.ssreflect.order]
Order.SigmaOrder.ltEsig [in mathcomp.ssreflect.order]
Order.SigmaOrder.lt_Taggedr [in mathcomp.ssreflect.order]
Order.SigmaOrder.lt_Taggedl [in mathcomp.ssreflect.order]
Order.SigmaOrder.lt_def [in mathcomp.ssreflect.order]
Order.SigmaOrder.refl [in mathcomp.ssreflect.order]
Order.SigmaOrder.topEsig [in mathcomp.ssreflect.order]
Order.SigmaOrder.total [in mathcomp.ssreflect.order]
Order.SigmaOrder.trans [in mathcomp.ssreflect.order]
Order.size_enum_ord [in mathcomp.ssreflect.order]
Order.SubPOrderTheory.leEsub [in mathcomp.ssreflect.order]
Order.SubPOrderTheory.le_wval [in mathcomp.ssreflect.order]
Order.SubPOrderTheory.ltEsub [in mathcomp.ssreflect.order]
Order.SubPOrderTheory.lt_wval [in mathcomp.ssreflect.order]
Order.SubPOrderTheory.lt_val [in mathcomp.ssreflect.order]
Order.TDistrLatticeTheory.cover_leIxr [in mathcomp.ssreflect.order]
Order.TDistrLatticeTheory.cover_leIxl [in mathcomp.ssreflect.order]
Order.TDistrLatticeTheory.leI2E [in mathcomp.ssreflect.order]
Order.TDistrLatticeTheory.leI2l_le [in mathcomp.ssreflect.order]
Order.TDistrLatticeTheory.leI2r_le [in mathcomp.ssreflect.order]
Order.TDistrLatticeTheory.meets_total [in mathcomp.ssreflect.order]
Order.TJoinTheory.joinx1 [in mathcomp.ssreflect.order]
Order.TJoinTheory.join1x [in mathcomp.ssreflect.order]
Order.TLatticeMorphismTheory.comp_is_top_morphism [in mathcomp.ssreflect.order]
Order.TLatticeMorphismTheory.idfun_is_top_morphism [in mathcomp.ssreflect.order]
Order.TLatticeMorphismTheory.omorph1 [in mathcomp.ssreflect.order]
Order.TMeetTheory.le_meets [in mathcomp.ssreflect.order]
Order.TMeetTheory.meetsP [in mathcomp.ssreflect.order]
Order.TMeetTheory.meetsP_seq [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_seq [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_setU [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_ge [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_max [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_inf [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_max_seq [in mathcomp.ssreflect.order]
Order.TMeetTheory.meets_inf_seq [in mathcomp.ssreflect.order]
Order.TMeetTheory.meetx1 [in mathcomp.ssreflect.order]
Order.TMeetTheory.meet_eq1 [in mathcomp.ssreflect.order]
Order.TMeetTheory.meet1x [in mathcomp.ssreflect.order]
Order.TotalTheory.arg_maxP [in mathcomp.ssreflect.order]
Order.TotalTheory.arg_minP [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxD [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxD1 [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxID [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxIl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxIr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxU [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxUl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmaxUr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_imset [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_set1 [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_eq_arg [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_ltP [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_leP [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_sup [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_eq_id [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_ge_id [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_idr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_idl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_split [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_mkcondr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_mkcondl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmax_mkcond [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminD [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminD1 [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminID [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminIl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminIr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminU [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminUl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigminUr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_imset [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_set1 [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_eq_arg [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_gtP [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_geP [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_inf [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_le [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_le_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_eq_id [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_le_id [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_idr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_idl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_split [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_mkcondr [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_mkcondl [in mathcomp.ssreflect.order]
Order.TotalTheory.bigmin_mkcond [in mathcomp.ssreflect.order]
Order.TotalTheory.comparableT [in mathcomp.ssreflect.order]
Order.TotalTheory.contraFle [in mathcomp.ssreflect.order]
Order.TotalTheory.contraFlt [in mathcomp.ssreflect.order]
Order.TotalTheory.contraNle [in mathcomp.ssreflect.order]
Order.TotalTheory.contraNlt [in mathcomp.ssreflect.order]
Order.TotalTheory.contraPle [in mathcomp.ssreflect.order]
Order.TotalTheory.contraPlt [in mathcomp.ssreflect.order]
Order.TotalTheory.contraTle [in mathcomp.ssreflect.order]
Order.TotalTheory.contraTlt [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_lt_le [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_le_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_le [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_ltn_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_ltn_le [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_leq_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_leq_le [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_not_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.contra_not_le [in mathcomp.ssreflect.order]
Order.TotalTheory.count_lt_ge [in mathcomp.ssreflect.order]
Order.TotalTheory.count_le_gt [in mathcomp.ssreflect.order]
Order.TotalTheory.DualTotalTheory.nth_count_eq [in mathcomp.ssreflect.order]
Order.TotalTheory.DualTotalTheory.nth_count_gt [in mathcomp.ssreflect.order]
Order.TotalTheory.DualTotalTheory.nth_count_ge [in mathcomp.ssreflect.order]
Order.TotalTheory.DualTotalTheory.sorted_filter_ge [in mathcomp.ssreflect.order]
Order.TotalTheory.DualTotalTheory.sorted_filter_gt [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_bigmax [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_bigmin [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_maxl [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_minr [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_ltRL [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_ltLR [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_leRL [in mathcomp.ssreflect.order]
Order.TotalTheory.eq_leLR [in mathcomp.ssreflect.order]
Order.TotalTheory.filter_sort_le [in mathcomp.ssreflect.order]
Order.TotalTheory.ge_max [in mathcomp.ssreflect.order]
Order.TotalTheory.ge_min [in mathcomp.ssreflect.order]
Order.TotalTheory.ge_total [in mathcomp.ssreflect.order]
Order.TotalTheory.gt_max [in mathcomp.ssreflect.order]
Order.TotalTheory.gt_min [in mathcomp.ssreflect.order]
Order.TotalTheory.joinEtotal [in mathcomp.ssreflect.order]
Order.TotalTheory.leIx [in mathcomp.ssreflect.order]
Order.TotalTheory.leNgt [in mathcomp.ssreflect.order]
Order.TotalTheory.lexU [in mathcomp.ssreflect.order]
Order.TotalTheory.le_nmono_in [in mathcomp.ssreflect.order]
Order.TotalTheory.le_mono_in [in mathcomp.ssreflect.order]
Order.TotalTheory.le_nmono [in mathcomp.ssreflect.order]
Order.TotalTheory.le_mono [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax2 [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin2 [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_ord_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_ord_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_ord [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_ord [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_nat_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_nat_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmax_nat [in mathcomp.ssreflect.order]
Order.TotalTheory.le_bigmin_nat [in mathcomp.ssreflect.order]
Order.TotalTheory.le_max [in mathcomp.ssreflect.order]
Order.TotalTheory.le_min [in mathcomp.ssreflect.order]
Order.TotalTheory.lteifNE [in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_maxl [in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_maxr [in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_minl [in mathcomp.ssreflect.order]
Order.TotalTheory.lteif_minr [in mathcomp.ssreflect.order]
Order.TotalTheory.ltIx [in mathcomp.ssreflect.order]
Order.TotalTheory.ltNge [in mathcomp.ssreflect.order]
Order.TotalTheory.ltUx [in mathcomp.ssreflect.order]
Order.TotalTheory.ltxI [in mathcomp.ssreflect.order]
Order.TotalTheory.ltxU [in mathcomp.ssreflect.order]
Order.TotalTheory.lt_max [in mathcomp.ssreflect.order]
Order.TotalTheory.lt_min [in mathcomp.ssreflect.order]
Order.TotalTheory.lt_total [in mathcomp.ssreflect.order]
Order.TotalTheory.mask_sort_le [in mathcomp.ssreflect.order]
Order.TotalTheory.maxA [in mathcomp.ssreflect.order]
Order.TotalTheory.maxAC [in mathcomp.ssreflect.order]
Order.TotalTheory.maxACA [in mathcomp.ssreflect.order]
Order.TotalTheory.maxC [in mathcomp.ssreflect.order]
Order.TotalTheory.maxCA [in mathcomp.ssreflect.order]
Order.TotalTheory.maxEge [in mathcomp.ssreflect.order]
Order.TotalTheory.maxEgt [in mathcomp.ssreflect.order]
Order.TotalTheory.maxKx [in mathcomp.ssreflect.order]
Order.TotalTheory.maxxK [in mathcomp.ssreflect.order]
Order.TotalTheory.max_minr [in mathcomp.ssreflect.order]
Order.TotalTheory.max_minl [in mathcomp.ssreflect.order]
Order.TotalTheory.max_idPl [in mathcomp.ssreflect.order]
Order.TotalTheory.meetEtotal [in mathcomp.ssreflect.order]
Order.TotalTheory.mem2_sort_le [in mathcomp.ssreflect.order]
Order.TotalTheory.minA [in mathcomp.ssreflect.order]
Order.TotalTheory.minAC [in mathcomp.ssreflect.order]
Order.TotalTheory.minACA [in mathcomp.ssreflect.order]
Order.TotalTheory.minC [in mathcomp.ssreflect.order]
Order.TotalTheory.minCA [in mathcomp.ssreflect.order]
Order.TotalTheory.minEge [in mathcomp.ssreflect.order]
Order.TotalTheory.minEgt [in mathcomp.ssreflect.order]
Order.TotalTheory.minKx [in mathcomp.ssreflect.order]
Order.TotalTheory.minxK [in mathcomp.ssreflect.order]
Order.TotalTheory.min_maxr [in mathcomp.ssreflect.order]
Order.TotalTheory.min_maxl [in mathcomp.ssreflect.order]
Order.TotalTheory.min_idPr [in mathcomp.ssreflect.order]
Order.TotalTheory.neq_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.perm_sort_leP [in mathcomp.ssreflect.order]
Order.TotalTheory.sorted_subseq_sort_le [in mathcomp.ssreflect.order]
Order.TotalTheory.sorted_mask_sort_le [in mathcomp.ssreflect.order]
Order.TotalTheory.sort_lt_sorted [in mathcomp.ssreflect.order]
Order.TotalTheory.sort_le_sorted [in mathcomp.ssreflect.order]
Order.TotalTheory.subseq_sort_le [in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmax_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmin_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmax [in mathcomp.ssreflect.order]
Order.TotalTheory.subset_bigmin [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_in_bigmax [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_in_bigmin [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmax_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmin_cond [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmax_seq [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmin_seq [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmax [in mathcomp.ssreflect.order]
Order.TotalTheory.sub_bigmin [in mathcomp.ssreflect.order]
Order.TotalTheory.wlog_lt [in mathcomp.ssreflect.order]
Order.TotalTheory.wlog_le [in mathcomp.ssreflect.order]
Order.TPOrderTheory.lex1 [in mathcomp.ssreflect.order]
Order.TPOrderTheory.le1x [in mathcomp.ssreflect.order]
Order.TPOrderTheory.ltx1 [in mathcomp.ssreflect.order]
Order.TPOrderTheory.lt1x [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.botEtlexi [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.lexi_tupleP [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.lex1 [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.le0x [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.ltxi_tuplePlt [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.ltxi_tupleP [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.sub_tprod_lexi [in mathcomp.ssreflect.order]
Order.TupleLexiOrder.topEtlexi [in mathcomp.ssreflect.order]
Order.TupleProdOrder.botEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.codiffErcompl [in mathcomp.ssreflect.order]
Order.TupleProdOrder.codiffEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.complEcodiff [in mathcomp.ssreflect.order]
Order.TupleProdOrder.complEdiff [in mathcomp.ssreflect.order]
Order.TupleProdOrder.complEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.diffErcompl [in mathcomp.ssreflect.order]
Order.TupleProdOrder.diffEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.joinEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.leEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.leUx [in mathcomp.ssreflect.order]
Order.TupleProdOrder.lexI [in mathcomp.ssreflect.order]
Order.TupleProdOrder.lex1 [in mathcomp.ssreflect.order]
Order.TupleProdOrder.le0x [in mathcomp.ssreflect.order]
Order.TupleProdOrder.ltEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.meetUl [in mathcomp.ssreflect.order]
Order.TupleProdOrder.rcomplEtprod [in mathcomp.ssreflect.order]
Order.TupleProdOrder.rcomplPjoin [in mathcomp.ssreflect.order]
Order.TupleProdOrder.rcomplPmeet [in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_compl [in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_codiff [in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_diff [in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_rcompl [in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_join [in mathcomp.ssreflect.order]
Order.TupleProdOrder.tnth_meet [in mathcomp.ssreflect.order]
Order.TupleProdOrder.topEtprod [in mathcomp.ssreflect.order]
Order.val_enum_ord [in mathcomp.ssreflect.order]
order1 [in mathcomp.fingroup.fingroup]
ordSK [in mathcomp.ssreflect.fintype]
ordS_inj [in mathcomp.ssreflect.fintype]
ordS_bij [in mathcomp.ssreflect.fintype]
ordS_subproof [in mathcomp.ssreflect.fintype]
ord_enum4 [in mathcomp.solvable.burnside_app]
ord_pred_inj [in mathcomp.ssreflect.fintype]
ord_pred_bij [in mathcomp.ssreflect.fintype]
ord_predK [in mathcomp.ssreflect.fintype]
ord_pred_subproof [in mathcomp.ssreflect.fintype]
ord_enum_uniq [in mathcomp.ssreflect.fintype]
ord_inj [in mathcomp.ssreflect.fintype]
ord1 [in mathcomp.algebra.zmodp]
ord1 [in mathcomp.ssreflect.fintype]
orthoDmx [in mathcomp.algebra.sesquilinear]
orthoDv [in mathcomp.algebra.sesquilinear]
orthogonalE [in mathcomp.algebra.sesquilinear]
orthogonalP [in mathcomp.character.classfun]
orthogonalP [in mathcomp.algebra.sesquilinear]
orthogonal_span [in mathcomp.character.vcharacter]
orthogonal_free [in mathcomp.character.classfun]
orthogonal_oppl [in mathcomp.character.classfun]
orthogonal_oppr [in mathcomp.character.classfun]
orthogonal_split [in mathcomp.character.classfun]
orthogonal_catr [in mathcomp.character.classfun]
orthogonal_catl [in mathcomp.character.classfun]
orthogonal_sym [in mathcomp.character.classfun]
orthogonal_cons [in mathcomp.character.classfun]
orthogonal_split [in mathcomp.algebra.sesquilinear]
orthogonal_oppl [in mathcomp.algebra.sesquilinear]
orthogonal_catr [in mathcomp.algebra.sesquilinear]
orthogonal_catl [in mathcomp.algebra.sesquilinear]
orthogonal_sym [in mathcomp.algebra.sesquilinear]
orthogonal_free [in mathcomp.algebra.sesquilinear]
orthogonal_oppr [in mathcomp.algebra.sesquilinear]
orthogonal_cons [in mathcomp.algebra.sesquilinear]
orthogonal1P [in mathcomp.algebra.sesquilinear]
orthomxD [in mathcomp.algebra.sesquilinear]
orthomxE [in mathcomp.algebra.sesquilinear]
orthomxN [in mathcomp.algebra.sesquilinear]
orthomxP [in mathcomp.algebra.sesquilinear]
orthomxZ [in mathcomp.algebra.sesquilinear]
orthomx_spectralP [in mathcomp.algebra.spectral]
orthomx_spectral_subproof [in mathcomp.algebra.spectral]
orthomx_proj_mx_ortho [in mathcomp.algebra.spectral]
orthomx_ortho_disj [in mathcomp.algebra.spectral]
orthomx_disj [in mathcomp.algebra.spectral]
orthomx_sym [in mathcomp.algebra.sesquilinear]
orthomx1E [in mathcomp.algebra.spectral]
orthomx1P [in mathcomp.algebra.spectral]
orthoNmx [in mathcomp.algebra.sesquilinear]
orthonormalE [in mathcomp.character.classfun]
orthonormalE [in mathcomp.algebra.sesquilinear]
orthonormalP [in mathcomp.character.classfun]
orthonormalP [in mathcomp.algebra.sesquilinear]
orthonormal_span [in mathcomp.character.vcharacter]
orthonormal_free [in mathcomp.character.classfun]
orthonormal_cat [in mathcomp.character.classfun]
orthonormal_orthogonal [in mathcomp.character.classfun]
orthonormal_not0 [in mathcomp.character.classfun]
orthonormal_free [in mathcomp.algebra.sesquilinear]
orthonormal_cat [in mathcomp.algebra.sesquilinear]
orthonormal_orthogonal [in mathcomp.algebra.sesquilinear]
orthonormal_not0 [in mathcomp.algebra.sesquilinear]
orthonormal2P [in mathcomp.character.classfun]
orthonormal2P [in mathcomp.algebra.sesquilinear]
orthoP [in mathcomp.character.classfun]
orthoP [in mathcomp.algebra.sesquilinear]
orthoPl [in mathcomp.character.classfun]
orthoPl [in mathcomp.algebra.sesquilinear]
orthoPr [in mathcomp.character.classfun]
orthoPr [in mathcomp.algebra.sesquilinear]
orthovD [in mathcomp.algebra.sesquilinear]
orthovE [in mathcomp.algebra.sesquilinear]
orthovP [in mathcomp.algebra.sesquilinear]
orthov_sym [in mathcomp.algebra.sesquilinear]
orthov0 [in mathcomp.algebra.sesquilinear]
orthov1E [in mathcomp.algebra.sesquilinear]
orthov11 [in mathcomp.algebra.sesquilinear]
orthoZmx [in mathcomp.algebra.sesquilinear]
ortho_id [in mathcomp.algebra.spectral]
ortho_mx_ortho [in mathcomp.algebra.sesquilinear]
ortho_ortho_mx [in mathcomp.algebra.sesquilinear]
out_perm [in mathcomp.fingroup.perm]
out_Aut [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 | (54001 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 | (1931 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 | (1658 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 | (7199 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 | (97 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 | (15214 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 | (75 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 | (224 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 | (2371 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 | (2266 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 | (732 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 | (21455 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 | (647 entries) |