'O' (Definitions)

Files

G

J

V

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

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 [def, in mathcomp.classical.classical_sets]
one_inum [def, in mathcomp.reals.itv]
one_point_compactification [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_compactification_one_point_compactification__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_point_nbhs [def, in mathcomp.analysis.topology_theory.one_point_compactification]
one_snum [def, in mathcomp.reals.signed]
onem [def, in mathcomp.classical.mathcomp_extra]
onem_nonneg [def, in mathcomp.reals.signed]
open [def, in mathcomp.analysis.topology_theory.topology_structure]
open_fam_of [def, in mathcomp.analysis.topology_theory.compact]
open_itv_cover [def, in mathcomp.classical.set_interval]
open_nbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
openE_subproof [def, in mathcomp.analysis.topology_theory.topology_structure]
Opp_bigO [def, in mathcomp.analysis.landau]
opp_inum [def, in mathcomp.reals.itv]
opp_itv_bound_subdef [def, in mathcomp.reals.itv]
opp_itv_subdef [def, in mathcomp.reals.itv]
opp_littleo [def, in mathcomp.analysis.landau]
opp_reality_subdef [def, in mathcomp.reals.signed]
opp_snum [def, in mathcomp.reals.signed]
oppe [def, in mathcomp.reals.constructive_ereal]
oppe_snum [def, in mathcomp.reals.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_isNbhs.identity_builder [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.order_topology]
Order_isNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Le_isPOrder__to__Order_isPOrder [def, in mathcomp.classical.classical_orders]
Order_max__canonical__Monoid_ComLaw [def, in mathcomp.reals.constructive_ereal]
Order_max__canonical__Monoid_Law [def, in mathcomp.reals.constructive_ereal]
Order_max_fun__canonical__cardinality_FImFun [def, in mathcomp.analysis.numfun]
Order_max_fun__canonical__HBNNSimple_NonNegSimpleFun [def, in mathcomp.analysis.lebesgue_integral]
Order_max_fun__canonical__HBSimple_SimpleFun [def, in mathcomp.analysis.lebesgue_integral]
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_POrder__to__choice_hasChoice [def, in mathcomp.reals.signed]
Order_POrder__to__eqtype_hasDecEq [def, in mathcomp.reals.signed]
Order_POrder__to__Order_isPOrder [def, in mathcomp.reals.signed]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.reals_stdlib.Rstruct]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.reals.signed]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.reals.constructive_ereal]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.classical.classical_orders]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.reals_stdlib.Rstruct]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.reals.signed]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.reals.constructive_ereal]
Order_POrder_isTotal__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.classical.classical_orders]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.reals_stdlib.Rstruct]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.reals.signed]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.reals.constructive_ereal]
Order_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.classical.classical_orders]
Order_SubChoice_isSubPOrder__to__Order_isPOrder [def, in mathcomp.reals.itv]
Order_SubChoice_isSubPOrder__to__Order_isSubPOrder [def, in mathcomp.reals.itv]
order_topology [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
order_topology_order_topology__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Total__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Total__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Total__to__Order_DistrLattice_isTotal [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Total__to__Order_isPOrder [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Total__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
Order_Total__to__Order_POrder_isLattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_filter_Filtered_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_filter_Filtered_and_Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_filter_Filtered_and_Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_filter_Nbhs_and_Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_filter_Nbhs_and_Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_Order_DistrLattice_and_filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_Order_DistrLattice_and_filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.join_order_topology_OrderNbhs_between_Order_Lattice_and_filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__choice_Choice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs__to__Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__Order_POrder_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.Exports.order_topology_OrderNbhs_class__to__Order_Total_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.pack_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.phant_clone [def, in mathcomp.analysis.topology_theory.order_topology]
OrderNbhs.phant_on_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_Order_DistrLattice_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_Order_Lattice_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_Order_POrder_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_order_topology_OrderNbhs_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_order_topology_OrderTopological_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_order_topology_OrderUniform_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.join_order_topology_OrderPseudoMetric_between_pseudometric_structure_PseudoMetric_and_Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__choice_Choice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__order_topology_OrderUniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__Order_POrder_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__order_topology_OrderNbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__order_topology_OrderTopological_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__order_topology_OrderUniform_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__Order_Total_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__pseudometric_structure_PseudoMetric_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.Exports.order_topology_OrderPseudoMetric_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.pack_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.phant_clone [def, in mathcomp.analysis.topology_theory.order_topology]
OrderPseudoMetric.phant_on_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.join_order_topology_OrderTopological_between_Order_DistrLattice_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.join_order_topology_OrderTopological_between_Order_Lattice_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.join_order_topology_OrderTopological_between_Order_POrder_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.join_order_topology_OrderTopological_between_order_topology_OrderNbhs_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.join_order_topology_OrderTopological_between_topology_structure_Topological_and_Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__choice_Choice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__Order_POrder_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__order_topology_OrderNbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__Order_Total_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.Exports.order_topology_OrderTopological_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.pack_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.phant_clone [def, in mathcomp.analysis.topology_theory.order_topology]
OrderTopological.phant_on_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.join_order_topology_OrderUniform_between_Order_DistrLattice_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.join_order_topology_OrderUniform_between_Order_Lattice_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.join_order_topology_OrderUniform_between_Order_POrder_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.join_order_topology_OrderUniform_between_order_topology_OrderNbhs_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.join_order_topology_OrderUniform_between_order_topology_OrderTopological_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.join_order_topology_OrderUniform_between_Order_Total_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__choice_Choice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__Order_Lattice [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__Order_POrder [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__Order_Total [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__Order_POrder_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__order_topology_OrderNbhs_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__order_topology_OrderTopological_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__Order_Total_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.Exports.order_topology_OrderUniform_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.pack_ [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.phant_clone [def, in mathcomp.analysis.topology_theory.order_topology]
OrderUniform.phant_on_ [def, in mathcomp.analysis.topology_theory.order_topology]
ordII [def, in mathcomp.classical.classical_sets]
ordIIK [def, in mathcomp.classical.classical_sets]
ortho [def, in mathcomp.analysis.forms]
OuO [def, in mathcomp.analysis_stdlib.showcase.uniform_bigO]
OuP [def, in mathcomp.analysis_stdlib.showcase.uniform_bigO]
OuPex [def, in mathcomp.analysis_stdlib.showcase.uniform_bigO]
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]