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 (54435 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 (7636 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 (72 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.o