'O' (Definitions)
| Files | 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 | _ | * |
| Definitions | 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 | _ | * |
| Lemmas | 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 | _ | * |
| Abbreviations | 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 | _ | * |
| 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 | _ | * |
O (Definitions)
OCan2.phant_axioms [def, in mathcomp.classical.functions]OCan2.phant_Build [def, in mathcomp.classical.functions]
OCanV.phant_axioms [def, in mathcomp.classical.functions]
OCanV.phant_Build [def, in mathcomp.classical.functions]
ocitv [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
ocitv_display [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
ocitv_type [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
oinv [def, in mathcomp.classical.functions]
OInv.identity_builder [def, in mathcomp.classical.functions]
OInv.phant_axioms [def, in mathcomp.classical.functions]
OInv.phant_Build [def, in mathcomp.classical.functions]
OInv_Can.identity_builder [def, in mathcomp.classical.functions]
OInv_Can.OInv_Can_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
OInv_Can.phant_axioms [def, in mathcomp.classical.functions]
OInv_Can.phant_Build [def, in mathcomp.classical.functions]
OInv_Can2.OInv_Can2_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
OInv_Can2.phant_axioms [def, in mathcomp.classical.functions]
OInv_Can2.phant_Build [def, in mathcomp.classical.functions]
OInv_CanV.identity_builder [def, in mathcomp.classical.functions]
OInv_CanV.OInv_CanV_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
OInv_CanV.phant_axioms [def, in mathcomp.classical.functions]
OInv_CanV.phant_Build [def, in mathcomp.classical.functions]
OInv_Inv.identity_builder [def, in mathcomp.classical.functions]
OInv_Inv.OInv_Inv_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
OInv_Inv.phant_axioms [def, in mathcomp.classical.functions]
OInv_Inv.phant_Build [def, in mathcomp.classical.functions]
OInversible.pack_ [def, in mathcomp.classical.functions]
OInversible.phant_clone [def, in mathcomp.classical.functions]
OInversible.phant_on_ [def, in mathcomp.classical.functions]
OInvFun.Exports.functions_OInvFun__to__functions_Fun [def, in mathcomp.classical.functions]
OInvFun.Exports.functions_OInvFun__to__functions_OInversible [def, in mathcomp.classical.functions]
OInvFun.Exports.functions_OInvFun_class__to__functions_Fun_class [def, in mathcomp.classical.functions]
OInvFun.Exports.functions_OInvFun_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
OInvFun.Exports.join_functions_OInvFun_between_functions_Fun_and_functions_OInversible [def, in mathcomp.classical.functions]
OInvFun.pack_ [def, in mathcomp.classical.functions]
OInvFun.phant_clone [def, in mathcomp.classical.functions]
OInvFun.phant_on_ [def, in mathcomp.classical.functions]
oinvK [def, in mathcomp.classical.functions]
oinvS [def, in mathcomp.classical.functions]
oliftV [def, in mathcomp.classical.functions]
one_inum [def, in mathcomp.analysis.itv]
one_snum [def, in mathcomp.analysis.signed]
onem [def, in mathcomp.classical.mathcomp_extra]
onem_nonneg [def, in mathcomp.analysis.signed]
open [def, in mathcomp.analysis.topology]
open_fam_of [def, in mathcomp.analysis.topology]
open_nbhs [def, in mathcomp.analysis.topology]
openE_subproof [def, in mathcomp.analysis.topology]
Opp_bigO [def, in mathcomp.analysis.landau]
opp_inum [def, in mathcomp.analysis.itv]
opp_itv_bound_subdef [def, in mathcomp.analysis.itv]
opp_itv_subdef [def, in mathcomp.analysis.itv]
opp_littleo [def, in mathcomp.analysis.landau]
opp_reality_subdef [def, in mathcomp.analysis.signed]
opp_snum [def, in mathcomp.analysis.signed]
oppe [def, in mathcomp.analysis.constructive_ereal]
oppe_snum [def, in mathcomp.analysis.constructive_ereal]
Option_apply__canonical__functions_Bij [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_Fun [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_Inject [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_Surject [def, in mathcomp.classical.functions]
Option_apply__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_Bij [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_Fun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_Inject [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_Surject [def, in mathcomp.classical.functions]
Option_bind__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_Bij [def, in mathcomp.classical.functions]
Option_default__canonical__functions_Fun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_Inject [def, in mathcomp.classical.functions]
Option_default__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Option_default__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Option_default__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Option_default__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Option_default__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Option_default__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Option_default__canonical__functions_Surject [def, in mathcomp.classical.functions]
Option_default__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_Bij [def, in mathcomp.classical.functions]
Option_map__canonical__functions_Fun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_Inject [def, in mathcomp.classical.functions]
Option_map__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Option_map__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Option_map__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Option_map__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Option_map__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Option_map__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Option_map__canonical__functions_Surject [def, in mathcomp.classical.functions]
Option_map__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Order.default_display [def, in mathcomp.classical.mathcomp_extra]
Order.disp_t [def, in mathcomp.classical.mathcomp_extra]
Order_max__canonical__Monoid_ComLaw [def, in mathcomp.analysis.constructive_ereal]
Order_max__canonical__Monoid_Law [def, in mathcomp.analysis.constructive_ereal]
Order_max_fun__canonical__cardinality_FImFun [def, in mathcomp.analysis.numfun]
Order_max_fun__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
Order_max_fun__canonical__lebesgue_integral_NonNegFun [def, in mathcomp.analysis.lebesgue_integral]
Order_max_fun__canonical__lebesgue_integral_NonNegSimpleFun [def, in mathcomp.analysis.lebesgue_integral]
Order_max_fun__canonical__lebesgue_integral_SimpleFun [def, in mathcomp.analysis.lebesgue_integral]
Order_POrder__to__choice_hasChoice [def, in mathcomp.analysis.signed]
Order_POrder__to__eqtype_hasDecEq [def, in mathcomp.analysis.signed]
Order_POrder__to__Order_isPOrder [def, in mathcomp.analysis.signed]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.analysis.Rstruct]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.analysis.signed]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.analysis.constructive_ereal]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.analysis.Rstruct]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.analysis.signed]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.analysis.constructive_ereal]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.analysis.Rstruct]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.analysis.signed]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.analysis.constructive_ereal]
Order_SubChoice_isSubPOrder__to__Order_isPOrder [def, in mathcomp.analysis.itv]
Order_SubChoice_isSubPOrder__to__Order_isSubPOrder [def, in mathcomp.analysis.itv]
ordII [def, in mathcomp.classical.classical_sets]
ordIIK [def, in mathcomp.classical.classical_sets]
ortho [def, in mathcomp.analysis.forms]
outer_measure0 [def, in mathcomp.analysis.measure]
outer_measure_ge0 [def, in mathcomp.analysis.measure]
outer_measure_sigma_subadditive [def, in mathcomp.analysis.measure]
OuterMeasure.pack_ [def, in mathcomp.analysis.measure]
OuterMeasure.phant_clone [def, in mathcomp.analysis.measure]
OuterMeasure.phant_on_ [def, in mathcomp.analysis.measure]
OuterMeasure_sort__canonical__measure_Content [def, in mathcomp.analysis.measure]
OuterMeasure_sort__canonical__measure_Measure [def, in mathcomp.analysis.measure]