'O' (Definitions)

Files

G

J

O

Q

U

V

X

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_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_itv_cover [def, in mathcomp.classical.set_interval]
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_isNbhs.identity_builder [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_DistrLattice [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_Lattice [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_POrder [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__Order_Total [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Order_isNbhs.Order_isNbhs_T__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Order_isNbhs.phant_axioms [def, in mathcomp.analysis.topology]
Order_isNbhs.phant_Build [def, in mathcomp.analysis.topology]
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.signed]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [def, in mathcomp.analysis.constructive_ereal]
Order_POrder_isTotal__to__Order_DistrLattice_isTotal [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_Lattice_Meet_isDistrLattice [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_POrder_isTotal__to__Order_POrder_isLattice [def, in mathcomp.analysis.Rstruct]
Order_SubChoice_isSubPOrder__to__Order_isPOrder [def, in mathcomp.analysis.itv]
Order_SubChoice_isSubPOrder__to__Order_isSubPOrder [def, in mathcomp.analysis.itv]
order_topology [def, in mathcomp.analysis.topology]
Order_Total__to__choice_hasChoice [def, in mathcomp.analysis.topology]
Order_Total__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology]
Order_Total__to__Order_DistrLattice_isTotal [def, in mathcomp.analysis.topology]
Order_Total__to__Order_isPOrder [def, in mathcomp.analysis.topology]
Order_Total__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.analysis.topology]
Order_Total__to__Order_POrder_isLattice [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_Order_DistrLattice_and_topology_Filtered [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_Order_DistrLattice_and_topology_Nbhs [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_Order_Lattice_and_topology_Nbhs [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_topology_Filtered_and_Order_Lattice [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_topology_Filtered_and_Order_POrder [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_topology_Filtered_and_Order_Total [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_topology_Nbhs_and_Order_POrder [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.join_topology_OrderNbhs_between_topology_Nbhs_and_Order_Total [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__choice_Choice [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__eqtype_Equality [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__Order_DistrLattice [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__Order_Lattice [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__Order_POrder [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__Order_Total [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__topology_Filtered [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs__to__topology_Nbhs [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__choice_Choice_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__Order_POrder_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__Order_Total_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__topology_Filtered_class [def, in mathcomp.analysis.topology]
OrderNbhs.Exports.topology_OrderNbhs_class__to__topology_Nbhs_class [def, in mathcomp.analysis.topology]
OrderNbhs.pack_ [def, in mathcomp.analysis.topology]
OrderNbhs.phant_clone [def, in mathcomp.analysis.topology]
OrderNbhs.phant_on_ [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_Order_DistrLattice_and_topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_Order_Lattice_and_topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_Order_POrder_and_topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_topology_OrderNbhs_and_topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_topology_OrderTopological_and_topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_topology_OrderUniform_and_topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.join_topology_OrderPseudoMetric_between_topology_PseudoMetric_and_Order_Total [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__choice_Choice [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__eqtype_Equality [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__Order_DistrLattice [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__Order_Lattice [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__Order_POrder [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__Order_Total [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_Filtered [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_Nbhs [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_OrderNbhs [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_OrderTopological [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_OrderUniform [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_PseudoMetric [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_Topological [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric__to__topology_Uniform [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__choice_Choice_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__Order_POrder_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__Order_Total_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_Filtered_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_Nbhs_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_OrderNbhs_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_OrderTopological_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_OrderUniform_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_PseudoMetric_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_Topological_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.Exports.topology_OrderPseudoMetric_class__to__topology_Uniform_class [def, in mathcomp.analysis.topology]
OrderPseudoMetric.pack_ [def, in mathcomp.analysis.topology]
OrderPseudoMetric.phant_clone [def, in mathcomp.analysis.topology]
OrderPseudoMetric.phant_on_ [def, in mathcomp.analysis.topology]
OrderTopological.Exports.join_topology_OrderTopological_between_Order_DistrLattice_and_topology_Topological [def, in mathcomp.analysis.topology]
OrderTopological.Exports.join_topology_OrderTopological_between_Order_Lattice_and_topology_Topological [def, in mathcomp.analysis.topology]
OrderTopological.Exports.join_topology_OrderTopological_between_Order_POrder_and_topology_Topological [def, in mathcomp.analysis.topology]
OrderTopological.Exports.join_topology_OrderTopological_between_topology_OrderNbhs_and_topology_Topological [def, in mathcomp.analysis.topology]
OrderTopological.Exports.join_topology_OrderTopological_between_topology_Topological_and_Order_Total [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__choice_Choice [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__eqtype_Equality [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__Order_DistrLattice [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__Order_Lattice [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__Order_POrder [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__Order_Total [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__topology_Filtered [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__topology_Nbhs [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__topology_OrderNbhs [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological__to__topology_Topological [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__choice_Choice_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__Order_POrder_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__Order_Total_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__topology_Filtered_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__topology_Nbhs_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__topology_OrderNbhs_class [def, in mathcomp.analysis.topology]
OrderTopological.Exports.topology_OrderTopological_class__to__topology_Topological_class [def, in mathcomp.analysis.topology]
OrderTopological.pack_ [def, in mathcomp.analysis.topology]
OrderTopological.phant_clone [def, in mathcomp.analysis.topology]
OrderTopological.phant_on_ [def, in mathcomp.analysis.topology]
OrderUniform.Exports.join_topology_OrderUniform_between_Order_DistrLattice_and_topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.join_topology_OrderUniform_between_Order_Lattice_and_topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.join_topology_OrderUniform_between_Order_POrder_and_topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.join_topology_OrderUniform_between_Order_Total_and_topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.join_topology_OrderUniform_between_topology_OrderNbhs_and_topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.join_topology_OrderUniform_between_topology_OrderTopological_and_topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__choice_Choice [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__eqtype_Equality [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__Order_DistrLattice [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__Order_Lattice [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__Order_POrder [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__Order_Total [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__topology_Filtered [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__topology_Nbhs [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__topology_OrderNbhs [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__topology_OrderTopological [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__topology_Topological [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform__to__topology_Uniform [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__choice_Choice_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__Order_POrder_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__Order_Total_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__topology_Filtered_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__topology_Nbhs_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__topology_OrderNbhs_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__topology_OrderTopological_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__topology_Topological_class [def, in mathcomp.analysis.topology]
OrderUniform.Exports.topology_OrderUniform_class__to__topology_Uniform_class [def, in mathcomp.analysis.topology]
OrderUniform.pack_ [def, in mathcomp.analysis.topology]
OrderUniform.phant_clone [def, in mathcomp.analysis.topology]
OrderUniform.phant_on_ [def, in mathcomp.analysis.topology]
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]