'R' (Definitions)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
R (Definitions)
R_isMeasurable [def, in mathcomp.analysis.lebesgue_measure]rad [def, in mathcomp.analysis.forms]
radius [def, in mathcomp.analysis.normedtype]
Radon_Nikodym [def, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f [def, in mathcomp.analysis.charge]
random_variable [def, in mathcomp.analysis.probability]
range1 [def, in mathcomp.analysis.reals]
rat_rat__canonical__classical_sets_Pointed [def, in mathcomp.classical.cardinality]
RbaseSymbolsImpl_R__canonical__choice_Choice [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__classical_sets_Pointed [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__eqtype_Equality [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__filter_Filtered [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__filter_Nbhs [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__filter_PointedFiltered [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__filter_PointedNbhs [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_ComRing [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_ComSemiRing [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_ComUnitRing [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Field [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_IntegralDomain [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Nmodule [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Ring [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_SemiRing [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_UnitRing [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Zmodule [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiDomain [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiField [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiNumDomain [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiNumField [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiRealClosedField [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_NormedZmodule [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_NumDomain [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_NumField [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_POrderedZmodule [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_RealClosedField [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_RealDomain [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_RealField [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_DistrLattice [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_Lattice [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_POrder [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_Total [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__reals_Real [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__topology_structure_Topological [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_R__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__Monoid_ComLaw [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__Monoid_Law [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__Monoid_MulLaw [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__SemiGroup_ComLaw [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__SemiGroup_Law [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__Monoid_AddLaw [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__Monoid_ComLaw [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__Monoid_Law [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__SemiGroup_ComLaw [def, in mathcomp.analysis.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__SemiGroup_Law [def, in mathcomp.analysis.Rstruct]
Rceil [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__choice_Choice [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__eqtype_Equality [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_ComRing [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_ComSemiRing [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_ComUnitRing [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_Field [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_IntegralDomain [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_Nmodule [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_Ring [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_SemiRing [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_UnitRing [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__GRing_Zmodule [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_ArchiDomain [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_ArchiField [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_ArchiNumDomain [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_ArchiNumField [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_ArchiRealClosedField [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_NormedZmodule [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_NumDomain [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_NumField [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_POrderedZmodule [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_RealClosedField [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_RealDomain [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Num_RealField [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Order_DistrLattice [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Order_Lattice [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Order_POrder [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real__to__Order_Total [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__choice_Choice_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__eqtype_Equality_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_ComRing_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_ComSemiRing_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_ComUnitRing_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_Field_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_IntegralDomain_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_Nmodule_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_Ring_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_SemiRing_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_UnitRing_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__GRing_Zmodule_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_ArchiDomain_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_ArchiField_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_ArchiNumDomain_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_ArchiNumField_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_ArchiRealClosedField_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_NormedZmodule_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_NumDomain_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_NumField_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_POrderedZmodule_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_RealClosedField_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_RealDomain_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Num_RealField_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Order_Lattice_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Order_POrder_class [def, in mathcomp.analysis.reals]
Real.Exports.reals_Real_class__to__Order_Total_class [def, in mathcomp.analysis.reals]
Real.pack_ [def, in mathcomp.analysis.reals]
Real.phant_clone [def, in mathcomp.analysis.reals]
Real.phant_on_ [def, in mathcomp.analysis.reals]
real_domain_typ [def, in mathcomp.analysis.signed]
real_field_typ [def, in mathcomp.analysis.signed]
real_mulr_infty [def, in mathcomp.analysis.constructive_ereal]
Real_sort__canonical__GRing_Lmodule [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_Measurable [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_RingOfSets [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_SigmaRing [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__normedtype_CompleteNormedModule [def, in mathcomp.analysis.normedtype]
Real_sort__canonical__normedtype_NormedModule [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__normedtype_PseudoMetricNormedZmod [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__pseudometric_structure_CompletePseudoMetric [def, in mathcomp.analysis.normedtype]
Real_sort__canonical__uniform_structure_Complete [def, in mathcomp.analysis.normedtype]
realfun_itvN_oppr__canonical__functions_Fun [def, in mathcomp.analysis.realfun]
reals_Rint_pred__canonical__GRing_AddClosed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_Mul2Closed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_MulClosed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_OppClosed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_Semiring2Closed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_SemiringClosed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_SmulClosed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_SubringClosed [def, in mathcomp.analysis.reals]
reals_Rint_pred__canonical__GRing_ZmodClosed [def, in mathcomp.analysis.reals]
regular_space [def, in mathcomp.analysis.separation_axioms]
relp [def, in mathcomp.classical.boolp]
Rfloor [def, in mathcomp.analysis.reals]
Rgeb [def, in mathcomp.analysis.Rstruct]
RGenCInfty.G [def, in mathcomp.analysis.lebesgue_measure]
RGenInftyO.G [def, in mathcomp.analysis.lebesgue_measure]
RGenOInfty.G [def, in mathcomp.analysis.lebesgue_measure]
RGenOpens.G [def, in mathcomp.analysis.lebesgue_measure]
Rgtb [def, in mathcomp.analysis.Rstruct]
Rhull [def, in mathcomp.analysis.normedtype]
riemannR [def, in mathcomp.analysis.exp]
RingOfSets.Exports.measure_RingOfSets__to__choice_Choice [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets__to__classical_sets_Pointed [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets__to__eqtype_Equality [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets__to__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets_class__to__choice_Choice_class [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets_class__to__classical_sets_Pointed_class [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets_class__to__eqtype_Equality_class [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets_class__to__measure_SemiRingOfSets_class [def, in mathcomp.analysis.measure]
RingOfSets.pack_ [def, in mathcomp.analysis.measure]
RingOfSets.phant_clone [def, in mathcomp.analysis.measure]
RingOfSets.phant_on_ [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.identity_builder [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.phant_axioms [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.phant_Build [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Rint [def, in mathcomp.analysis.reals]
Rint_pred [def, in mathcomp.analysis.reals]
Rintegral [def, in mathcomp.analysis.lebesgue_integral]
Rinvx [def, in mathcomp.analysis.Rstruct]
Rleb [def, in mathcomp.analysis.Rstruct]
Rltb [def, in mathcomp.analysis.Rstruct]
root_mean_square [def, in mathcomp.analysis.sequences]
rpickle [def, in mathcomp.analysis.altreals.discrete]
Rtoint [def, in mathcomp.analysis.reals]
runpickle [def, in mathcomp.analysis.altreals.discrete]