'D' (Definitions)

Files

J

V

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

D (Definitions)

dadde_snum [def, in mathcomp.reals.constructive_ereal]
Datatypes_bool__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_bool__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscretePseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_PointedDiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_PointedDiscreteTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__filter_Filtered [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__filter_Nbhs [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__filter_PointedFiltered [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__filter_PointedNbhs [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__order_topology_OrderPseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__order_topology_OrderUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_Empty_set__canonical__classical_sets_Empty [def, in mathcomp.classical.classical_sets]
Datatypes_nat__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_nat__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscretePseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_PointedDiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_PointedDiscreteTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__order_topology_OrderPseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__order_topology_OrderUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_option__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_prod__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_prod__canonical__filter_Filtered [def, in mathcomp.classical.filter]
Datatypes_prod__canonical__filter_Nbhs [def, in mathcomp.classical.filter]
Datatypes_prod__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__normedtype_NormedModule [def, in mathcomp.analysis.normedtype]
Datatypes_prod__canonical__normedtype_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype]
Datatypes_prod__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.product_topology]
Datatypes_prod__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.product_topology]
Datatypes_prod__canonical__tvs_Tvs [def, in mathcomp.analysis.tvs]
Datatypes_prod__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.product_topology]
Datatypes_Some__canonical__functions_Bij [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_Fun [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_Inject [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_Surject [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Datatypes_unit__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_unit__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
davg [def, in mathcomp.analysis.lebesgue_integral]
dcvg [def, in mathcomp.experimental_reals.distr]
decode [def, in mathcomp.reals.constructive_ereal]
dEFin [def, in mathcomp.reals.constructive_ereal]
dEFin_snum [def, in mathcomp.reals.constructive_ereal]
dense [def, in mathcomp.analysis.topology_theory.topology_structure]
derivable [def, in mathcomp.analysis.derive]
derivable_oo_continuous_bnd [def, in mathcomp.analysis.realfun]
derive [def, in mathcomp.analysis.derive]
derive1 [def, in mathcomp.analysis.derive]
derive1n [def, in mathcomp.analysis.derive]
dflip [def, in mathcomp.experimental_reals.distr]
dfwith [def, in mathcomp.classical.mathcomp_extra]
diagonal [def, in mathcomp.classical.classical_sets]
diff [def, in mathcomp.analysis.derive]
dinsupp [def, in mathcomp.experimental_reals.distr]
dirac [def, in mathcomp.analysis.measure]
discontinuity [def, in mathcomp.analysis.realfun]
discrete_ball [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_ent [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_measurable [def, in mathcomp.analysis.measure]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_pred_sub__canonical__choice_Choice [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__choice_Countable [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__choice_SubChoice [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__choice_SubCountable [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__eqtype_Equality [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__eqtype_SubEquality [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__eqtype_SubType [def, in mathcomp.experimental_reals.discrete]
discrete_random_variable [def, in mathcomp.analysis.probability]
discrete_topology [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_Discrete_ofNbhs__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_Discrete_ofNbhs__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_Discrete_ofNbhs__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_discrete_topology__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscretePseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__discrete_topology_Discrete_ofPseudometric [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__discrete_topology_Discrete_ofPseudometric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__discrete_topology_Discrete_ofPseudometric [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__pseudometric_structure_Uniform_isPseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__pseudometric_structure_Uniform_isPseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__pseudometric_structure_Uniform_isPseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_DiscreteTopology__to__choice_hasChoice [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__discrete_topology_Discrete_ofNbhs [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__eqtype_hasDecEq [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__filter_isFiltered [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__filter_selfFiltered [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteUniform_ofNbhs__to__discrete_topology_Discrete_ofUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__discrete_topology_Discrete_ofUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__discrete_topology_Discrete_ofUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology_theory.bool_topology]
discreteMeasurableFun.Exports.probability_discreteMeasurableFun__to__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.probability]
discreteMeasurableFun.Exports.probability_discreteMeasurableFun_class__to__lebesgue_integral_MeasurableFun_class [def, in mathcomp.analysis.probability]
discreteMeasurableFun.pack_ [def, in mathcomp.analysis.probability]
discreteMeasurableFun.phant_clone [def, in mathcomp.analysis.probability]
discreteMeasurableFun.phant_on_ [def, in mathcomp.analysis.probability]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__discrete_topology_DiscreteTopology_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_JoinSemilattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_MeetSemilattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_POrder_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__order_topology_OrderNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__order_topology_OrderTopological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_Total_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__discrete_topology_DiscreteTopology_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__discrete_topology_DiscreteUniform_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__pseudometric_structure_PseudoMetric_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteNbhs_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteTopology_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteUniform_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.join_discrete_topology_DiscreteTopology_between_discrete_topology_DiscreteNbhs_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__discrete_topology_DiscreteTopology_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.join_discrete_topology_DiscreteUniform_between_discrete_topology_DiscreteNbhs_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.join_discrete_topology_DiscreteUniform_between_discrete_topology_DiscreteTopology_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
disj_set [def, in mathcomp.classical.classical_sets]
disjoint_itv [def, in mathcomp.classical.set_interval]
distr_of [def, in mathcomp.experimental_reals.distr]
distribution [def, in mathcomp.analysis.probability]
diter [def, in mathcomp.experimental_reals.distr]
dlet [def, in mathcomp.experimental_reals.distr]
dlift [def, in mathcomp.experimental_reals.distr]
dlim [def, in mathcomp.experimental_reals.distr]
dlim_bump [def, in mathcomp.experimental_reals.distr]
dlim_lift [def, in mathcomp.experimental_reals.distr]
dmargin [def, in mathcomp.experimental_reals.distr]
dnbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
dnbhs_filter_on [def, in mathcomp.analysis.topology_theory.topology_structure]
dnull [def, in mathcomp.experimental_reals.distr]
dominated_by [def, in mathcomp.analysis.normedtype]
double_snum [def, in mathcomp.reals.signed]
down [def, in mathcomp.classical.classical_sets]
drat [def, in mathcomp.experimental_reals.distr]
drestr [def, in mathcomp.experimental_reals.distr]
dRV_dom [def, in mathcomp.analysis.probability]
dRV_enum [def, in mathcomp.analysis.probability]
dswap [def, in mathcomp.experimental_reals.distr]
dual_adde [def, in mathcomp.reals.constructive_ereal]
dual_extended [def, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.constructive_ereal_dEFin__canonical__GRing_Additive [def, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.HB_unnamed_factory_43 [def, in mathcomp.reals.constructive_ereal]
ducvg [def, in mathcomp.experimental_reals.distr]
duni [def, in mathcomp.experimental_reals.distr]
dunit [def, in mathcomp.experimental_reals.distr]
dyadic_approx [def, in mathcomp.analysis.lebesgue_integral]
dyadic_itv [def, in mathcomp.analysis.lebesgue_integral]
dynkin [def, in mathcomp.analysis.measure]