'R' (Global Index)

Files

J

V

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

R

R1_neq_0 [prf, in mathcomp.reals_stdlib.Rstruct]
R_complete [prf, in mathcomp.analysis.normedtype]
R_fieldMixin [prf, in mathcomp.reals_stdlib.Rstruct]
r_gt0 [abbrev, in mathcomp.analysis.normedtype]
R_idomainMixin [prf, in mathcomp.reals_stdlib.Rstruct]
R_isMeasurable [def, in mathcomp.analysis.lebesgue_measure]
R_total [prf, in mathcomp.reals_stdlib.Rstruct]
rad [def, in mathcomp.analysis.forms]
rad_ker [prf, in mathcomp.analysis.forms]
radius [def, in mathcomp.analysis.normedtype]
radius0 [prf, in mathcomp.analysis.normedtype]
radius_ball [prf, in mathcomp.analysis.normedtype]
radius_ball_num [prf, in mathcomp.analysis.normedtype]
radius_scale_ball [prf, in mathcomp.analysis.normedtype]
Radon_Nikodym [def, in mathcomp.analysis.charge]
Radon_Nikodym0 [prf, in mathcomp.analysis.charge]
Radon_Nikodym_cadd [prf, in mathcomp.analysis.charge]
Radon_Nikodym_chain_rule [prf, in mathcomp.analysis.charge]
Radon_Nikodym_change_of_variables [prf, in mathcomp.analysis.charge]
Radon_Nikodym_cscale [prf, in mathcomp.analysis.charge]
Radon_Nikodym_fin_num [prf, in mathcomp.analysis.charge]
radon_nikodym_finite [prf, in mathcomp.analysis.charge]
Radon_Nikodym_integrable [prf, in mathcomp.analysis.charge]
Radon_Nikodym_integral [prf, in mathcomp.analysis.charge]
radon_nikodym_sigma_finite [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite [mod, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.chain_rule [prf, in mathcomp.analysis.charge]
'd '/d [not, in mathcomp.analysis.charge] (no scope)
Radon_Nikodym_SigmaFinite.change_of_variables [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f [def, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_fin_num [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_ge0 [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_integrable [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_integral [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.integrableM [prf, in mathcomp.analysis.charge]
'd '/d [not, in mathcomp.analysis.charge] (no scope)
Radon_NikodymE [prf, in mathcomp.analysis.charge]
random_variable [def, in mathcomp.analysis.probability]
range [abbrev, in mathcomp.classical.classical_sets]
range1 [def, in mathcomp.reals.reals]
range1rr [prf, in mathcomp.reals.reals]
range1z_inj [prf, in mathcomp.reals.reals]
range1zP [prf, in mathcomp.reals.reals]
range_factor [prf, in mathcomp.classical.set_interval]
range_line_path [prf, in mathcomp.classical.set_interval]
range_oppe [prf, in mathcomp.analysis.ereal]
rank_normal [prf, in mathcomp.analysis.forms]
Rarchimedean_axiom [prf, in mathcomp.reals_stdlib.Rstruct]
rat_in_itvoo [prf, in mathcomp.reals.reals]
rat_rat__canonical__classical_sets_Pointed [def, in mathcomp.classical.cardinality]
rational [def, in mathcomp.analysis.pi_irrational]
RbaseSymbolsImpl_R__canonical__choice_Choice [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__classical_sets_Pointed [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__eqtype_Equality [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__filter_Filtered [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__filter_Nbhs [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__filter_PointedFiltered [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__filter_PointedNbhs [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__GRing_ComRing [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_ComSemiRing [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_ComUnitRing [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Field [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_IntegralDomain [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Nmodule [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Ring [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_SemiRing [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_UnitRing [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__GRing_Zmodule [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiNumDomain [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiNumField [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiRealClosedField [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiRealDomain [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_ArchiRealField [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_NormedZmodule [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_NumDomain [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_NumField [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_POrderedZmodule [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_RealClosedField [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_RealDomain [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Num_RealField [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_DistrLattice [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_JoinSemilattice [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_Lattice [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_MeetSemilattice [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_POrder [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__Order_Total [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__reals_Real [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_R__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__topology_structure_Topological [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_R__canonical__uniform_structure_Uniform [def, in mathcomp.analysis_stdlib.Rstruct_topology]
RbaseSymbolsImpl_Rmult__canonical__Monoid_ComLaw [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__Monoid_Law [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__Monoid_MulLaw [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__SemiGroup_ComLaw [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rmult__canonical__SemiGroup_Law [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__Monoid_AddLaw [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__Monoid_ComLaw [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__Monoid_Law [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__SemiGroup_ComLaw [def, in mathcomp.reals_stdlib.Rstruct]
RbaseSymbolsImpl_Rplus__canonical__SemiGroup_Law [def, in mathcomp.reals_stdlib.Rstruct]
Rceil [def, in mathcomp.reals.reals]
Rceil0 [prf, in mathcomp.reals.reals]
Rceil_ge [prf, in mathcomp.reals.reals]
Rceil_ge0 [prf, in mathcomp.reals.reals]
RceilE [prf, in mathcomp.reals.reals]
Rcondcomplete [prf, in mathcomp.reals_stdlib.Rstruct]
RdivE [prf, in mathcomp.reals_stdlib.Rstruct]
Real [mod, in mathcomp.reals.reals]
Real.axioms_ [rec, in mathcomp.reals.reals]
Real.choice_hasChoice_mixin [proj, in mathcomp.reals.reals]
Real.class [proj, in mathcomp.reals.reals]
Real.eqtype_hasDecEq_mixin [proj, in mathcomp.reals.reals]
Real.Exports [mod, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__choice_Choice [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__eqtype_Equality [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_ComRing [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_ComSemiRing [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_ComUnitRing [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_Field [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_IntegralDomain [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_Nmodule [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_Ring [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_SemiRing [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_UnitRing [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__GRing_Zmodule [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_ArchiNumDomain [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_ArchiNumField [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_ArchiRealClosedField [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_ArchiRealDomain [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_ArchiRealField [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_NormedZmodule [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_NumDomain [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_NumField [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_POrderedZmodule [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_RealClosedField [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_RealDomain [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Num_RealField [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Order_DistrLattice [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Order_JoinSemilattice [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Order_Lattice [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Order_MeetSemilattice [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Order_POrder [def, in mathcomp.reals.reals]
Real.Exports.reals_Real__to__Order_Total [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__choice_Choice_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__eqtype_Equality_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_ComRing_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_ComSemiRing_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_ComUnitRing_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_Field_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_IntegralDomain_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_Nmodule_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_Ring_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_SemiRing_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_UnitRing_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__GRing_Zmodule_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_ArchiNumDomain_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_ArchiNumField_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_ArchiRealClosedField_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_ArchiRealDomain_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_ArchiRealField_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_NormedZmodule_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_NumDomain_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_NumField_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_POrderedZmodule_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_RealClosedField_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_RealDomain_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Num_RealField_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Order_DistrLattice_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Order_JoinSemilattice_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Order_Lattice_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Order_MeetSemilattice_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Order_POrder_class [def, in mathcomp.reals.reals]
Real.Exports.reals_Real_class__to__Order_Total_class [def, in mathcomp.reals.reals]
Real.GRing_ComUnitRing_isIntegral_mixin [proj, in mathcomp.reals.reals]
Real.GRing_isNmodule_mixin [proj, in mathcomp.reals.reals]
Real.GRing_Nmodule_isSemiRing_mixin [proj, in mathcomp.reals.reals]
Real.GRing_Nmodule_isZmodule_mixin [proj, in mathcomp.reals.reals]
Real.GRing_Ring_hasMulInverse_mixin [proj, in mathcomp.reals.reals]
Real.GRing_SemiRing_hasCommutativeMul_mixin [proj, in mathcomp.reals.reals]
Real.GRing_UnitRing_isField_mixin [proj, in mathcomp.reals.reals]
Real.Num_isNumRing_mixin [proj, in mathcomp.reals.reals]
Real.Num_NumDomain_isArchimedean_mixin [proj, in mathcomp.reals.reals]
Real.Num_RealField_isClosed_mixin [proj, in mathcomp.reals.reals]
Real.Num_Zmodule_isNormed_mixin [proj, in mathcomp.reals.reals]
Real.Order_DistrLattice_isTotal_mixin [proj, in mathcomp.reals.reals]
Real.Order_isDuallyPOrder_mixin [proj, in mathcomp.reals.reals]
Real.Order_Lattice_isDistributive_mixin [proj, in mathcomp.reals.reals]
Real.Order_POrder_isJoinSemilattice_mixin [proj, in mathcomp.reals.reals]
Real.Order_POrder_isMeetSemilattice_mixin [proj, in mathcomp.reals.reals]
Real.pack_ [def, in mathcomp.reals.reals]
Real.phant_clone [def, in mathcomp.reals.reals]
Real.phant_on_ [def, in mathcomp.reals.reals]
Real.reals_ArchimedeanField_isReal_mixin [proj, in mathcomp.reals.reals]
Real.sort [proj, in mathcomp.reals.reals]
Real.type [rec, in mathcomp.reals.reals]
real_cvgr_ge [prf, in mathcomp.analysis.normedtype]
real_cvgr_gt [prf, in mathcomp.analysis.normedtype]
real_cvgr_le [prf, in mathcomp.analysis.normedtype]
real_cvgr_lt [prf, in mathcomp.analysis.normedtype]
real_domain_typ [def, in mathcomp.reals.signed]
real_field_typ [def, in mathcomp.reals.signed]
real_interval [file, in mathcomp.reals.real_interval]
real_leey [prf, in mathcomp.reals.constructive_ereal]
real_leNye [prf, in mathcomp.reals.constructive_ereal]
real_ltNyr [prf, in mathcomp.reals.constructive_ereal]
real_ltr_distlC [prf, in mathcomp.classical.mathcomp_extra]
real_ltry [prf, in mathcomp.reals.constructive_ereal]
real_mulNyr [prf, in mathcomp.reals.constructive_ereal]
real_mulr_infty [def, in mathcomp.reals.constructive_ereal]
real_mulrNy [prf, in mathcomp.reals.constructive_ereal]
real_mulry [prf, in mathcomp.reals.constructive_ereal]
real_mulyr [prf, in mathcomp.reals.constructive_ereal]
real_order_nbhsE [prf, in mathcomp.analysis.topology_theory.num_topology]
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__pseudometric_structure_CompletePseudoMetric [def, in mathcomp.analysis.normedtype]
Real_sort__canonical__uniform_structure_Complete [def, in mathcomp.analysis.normedtype]
real_sup_adherent [prf, in mathcomp.reals_stdlib.Rstruct]
realDe [prf, in mathcomp.reals.constructive_ereal]
RealElpiOperations [mod, in mathcomp.reals.reals]
realfun [file, in mathcomp.analysis.realfun]
realfun_itvN_oppr__canonical__functions_Fun [def, in mathcomp.analysis.realfun]
realMe [prf, in mathcomp.reals.constructive_ereal]
reals [file, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_AddClosed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_Mul2Closed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_MulClosed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_OppClosed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_Semiring2Closed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_SemiringClosed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_SmulClosed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_SubringClosed [def, in mathcomp.reals.reals]
reals_Rint_pred__canonical__GRing_ZmodClosed [def, in mathcomp.reals.reals]
realseq [file, in mathcomp.experimental_reals.realseq]
realsum [file, in mathcomp.experimental_reals.realsum]
reflect_eq [prf, in mathcomp.classical.boolp]
regclosed [def, in mathcomp.analysis.topology_theory.topology_structure]
regopen [def, in mathcomp.analysis.topology_theory.topology_structure]
regular_openP [prf, in mathcomp.analysis.normedtype]
regular_space [def, in mathcomp.analysis.separation_axioms]
reindex_bigcap [prf, in mathcomp.classical.functions]
reindex_bigcup [prf, in mathcomp.classical.functions]
reindex_esum [prf, in mathcomp.analysis.esum]
reindex_fsbig [prf, in mathcomp.classical.fsbigop]
reindex_fsbigT [prf, in mathcomp.classical.fsbigop]
reindex_inside [abbrev, in mathcomp.classical.fsbigop]
reindex_inside_setT [abbrev, in mathcomp.classical.fsbigop]
reindex_psum [prf, in mathcomp.experimental_reals.realsum]
reindex_psum_onto [prf, in mathcomp.experimental_reals.realsum]
relp [def, in mathcomp.classical.boolp]
reparameterize [def, in mathcomp.analysis.homotopy_theory.continuous_path]
repr_comp_continuous [prf, in mathcomp.analysis.topology_theory.quotient_topology]
Req_EM_T [prf, in mathcomp.reals_stdlib.Rstruct]
restr [abbrev, in mathcomp.analysis.measure]
restr [abbrev, in mathcomp.analysis.measure]
restr [abbrev, in mathcomp.analysis.measure]
restr [abbrev, in mathcomp.analysis.charge]
restr [abbrev, in mathcomp.analysis.charge]
restrict [abbrev, in mathcomp.classical.functions]
restrict [abbrev, in mathcomp.classical.functions]
restrict_abse [prf, in mathcomp.analysis.ereal]
restrict_comp [prf, in mathcomp.classical.functions]
restrict_EFin [prf, in mathcomp.analysis.ereal]
restrict_ge0 [prf, in mathcomp.analysis.numfun]
restrict_indic [prf, in mathcomp.analysis.numfun]
restrict_lee [prf, in mathcomp.analysis.numfun]
restrict_normr [prf, in mathcomp.analysis.numfun]
restrict_set0 [prf, in mathcomp.analysis.numfun]
restricted_cvgE [prf, in mathcomp.analysis.function_spaces]
Rfloor [def, in mathcomp.reals.reals]
Rfloor0 [prf, in mathcomp.reals.reals]
Rfloor1 [prf, in mathcomp.reals.reals]
Rfloor_ge_int [prf, in mathcomp.reals.reals]
Rfloor_le [prf, in mathcomp.reals.reals]
Rfloor_le0 [prf, in mathcomp.reals.reals]
Rfloor_lt0 [prf, in mathcomp.reals.reals]
Rfloor_lt_int [prf, in mathcomp.reals.reals]
Rfloor_natz [prf, in mathcomp.reals.reals]
RfloorE [prf, in mathcomp.reals.reals]
Rgeb [def, in mathcomp.reals_stdlib.Rstruct]
RGenCInfty [mod, in mathcomp.analysis.lebesgue_measure]
RGenCInfty.G [def, in mathcomp.analysis.lebesgue_measure]
RGenCInfty.measurable_itv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
RGenCInfty.measurable_itv_bounded [prf, in mathcomp.analysis.lebesgue_measure]
RGenCInfty.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
RGenInftyO [mod, in mathcomp.analysis.lebesgue_measure]
RGenInftyO.G [def, in mathcomp.analysis.lebesgue_measure]
RGenInftyO.measurable_itv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
RGenInftyO.measurable_itv_bounded [prf, in mathcomp.analysis.lebesgue_measure]
RGenInftyO.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
RGenOInfty [mod, in mathcomp.analysis.lebesgue_measure]
RGenOInfty.G [def, in mathcomp.analysis.lebesgue_measure]
RGenOInfty.measurable_itv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
RGenOInfty.measurable_itv_bounded [prf, in mathcomp.analysis.lebesgue_measure]
RGenOInfty.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
RGenOpens [mod, in mathcomp.analysis.lebesgue_measure]
RGenOpens.G [def, in mathcomp.analysis.lebesgue_measure]
RGenOpens.measurable_itv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
RGenOpens.measurable_itv_bounded [prf, in mathcomp.analysis.lebesgue_measure]
RGenOpens.measurable_itv_infty_bnd [prf, in mathcomp.analysis.lebesgue_measure]
RGenOpens.measurable_itv_o_infty [prf, in mathcomp.analysis.lebesgue_measure]
RGenOpens.measurable_itvoo [prf, in mathcomp.analysis.lebesgue_measure]
RGenOpens.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
Rgtb [def, in mathcomp.reals_stdlib.Rstruct]
Rhausdorff [prf, in mathcomp.analysis.separation_axioms]
Rhull [def, in mathcomp.analysis.normedtype]
Rhull0 [prf, in mathcomp.analysis.normedtype]
Rhull_involutive [prf, in mathcomp.analysis.normedtype]
Rhull_smallest [prf, in mathcomp.analysis.normedtype]
RhullK [prf, in mathcomp.analysis.normedtype]
RhullT [prf, in mathcomp.analysis.normedtype]
riemannR [def, in mathcomp.analysis.exp]
riemannR_gt0 [prf, in mathcomp.analysis.exp]
right_bounded_interior [prf, in mathcomp.analysis.normedtype]
right_continuous [abbrev, in mathcomp.analysis.lebesgue_stieltjes_measure]
right_continuousW [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
ring_semi_sigma_additive [prf, in mathcomp.analysis.measure]
ring_sigma_sub_additive [abbrev, in mathcomp.analysis.measure]
ring_sigma_subadditive [prf, in mathcomp.analysis.measure]
RingOfSets [mod, in mathcomp.analysis.measure]
RingOfSets.axioms_ [rec, in mathcomp.analysis.measure]
RingOfSets.choice_hasChoice_mixin [proj, in mathcomp.analysis.measure]
RingOfSets.class [proj, in mathcomp.analysis.measure]
RingOfSets.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.measure]
RingOfSets.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.measure]
RingOfSets.Exports [mod, in mathcomp.analysis.measure]
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.measure_isSemiRingOfSets_mixin [proj, in mathcomp.analysis.measure]
RingOfSets.measure_SemiRingOfSets_isRingOfSets_mixin [proj, 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.sort [proj, in mathcomp.analysis.measure]
RingOfSets.type [rec, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets [mod, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.axioms_ [rec, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.Exports [mod, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.identity_builder [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.measurableT [proj, 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]
RingOfSetsElpiOperations [mod, in mathcomp.analysis.measure]
Rint [def, in mathcomp.reals.reals]
Rint0 [prf, in mathcomp.reals.reals]
Rint1 [prf, in mathcomp.reals.reals]
Rint_def [prf, in mathcomp.reals.reals]
Rint_ler_addr1 [prf, in mathcomp.reals.reals]
Rint_ltr_addr1 [prf, in mathcomp.reals.reals]
Rint_pred [def, in mathcomp.reals.reals]
Rint_subring_closed [prf, in mathcomp.reals.reals]
RintC [prf, in mathcomp.reals.reals]
Rintegral [def, in mathcomp.analysis.lebesgue_integral]
Rintegral_cst [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_ge0 [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_itv_bndo_bndc [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_itv_obnd_cbnd [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_itvB [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_mkcond [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_mkcondl [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_mkcondr [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_set0 [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_set1 [prf, in mathcomp.analysis.lebesgue_integral]
Rintegral_setU_EFin [prf, in mathcomp.analysis.lebesgue_integral]
RintegralB [prf, in mathcomp.analysis.lebesgue_integral]
RintegralZl [prf, in mathcomp.analysis.lebesgue_integral]
RintegralZr [prf, in mathcomp.analysis.lebesgue_integral]
Rintegration_by_parts [prf, in mathcomp.analysis.ftc]
RintP [prf, in mathcomp.reals.reals]
RinvE [prf, in mathcomp.reals_stdlib.Rstruct]
Rinvx [def, in mathcomp.reals_stdlib.Rstruct]
Rinvx_out [prf, in mathcomp.reals_stdlib.Rstruct]
RinvxRmult [prf, in mathcomp.reals_stdlib.Rstruct]
rl [abbrev, in mathcomp.classical.functions]
Rleb [def, in mathcomp.reals_stdlib.Rstruct]
Rleb_def [prf, in mathcomp.reals_stdlib.Rstruct]
Rleb_leVge [prf, in mathcomp.reals_stdlib.Rstruct]
Rleb_norm_add [prf, in mathcomp.reals_stdlib.Rstruct]
RlebP [prf, in mathcomp.reals_stdlib.Rstruct]
RleP [prf, in mathcomp.reals_stdlib.Rstruct]
Rltb [def, in mathcomp.reals_stdlib.Rstruct]
Rltb_def [prf, in mathcomp.reals_stdlib.Rstruct]
RltbP [prf, in mathcomp.reals_stdlib.Rstruct]
RltP [prf, in mathcomp.reals_stdlib.Rstruct]
RmaxE [prf, in mathcomp.reals_stdlib.Rstruct]
RminE [prf, in mathcomp.reals_stdlib.Rstruct]
RminusE [prf, in mathcomp.reals_stdlib.Rstruct]
Rmu [abbrev, in mathcomp.analysis.measure]
Rmu [abbrev, in mathcomp.analysis.measure]
Rmu_ext [prf, in mathcomp.analysis.measure]
RmultA [prf, in mathcomp.reals_stdlib.Rstruct]
RmultE [prf, in mathcomp.reals_stdlib.Rstruct]
RmultRinvx [prf, in mathcomp.reals_stdlib.Rstruct]
Rnorm0_eq0 [prf, in mathcomp.reals_stdlib.Rstruct]
RnormM [prf, in mathcomp.reals_stdlib.Rstruct]
Rolle [prf, in mathcomp.analysis.derive]
root_mean_square [def, in mathcomp.analysis.sequences]
RoppE [prf, in mathcomp.reals_stdlib.Rstruct]
rpickle [def, in mathcomp.experimental_reals.discrete]
rpickleK [prf, in mathcomp.experimental_reals.discrete]
RplusA [prf, in mathcomp.reals_stdlib.Rstruct]
RplusE [prf, in mathcomp.reals_stdlib.Rstruct]
RpowE [prf, in mathcomp.reals_stdlib.Rstruct]
rr [abbrev, in mathcomp.classical.functions]
rray_closed [prf, in mathcomp.analysis.topology_theory.order_topology]
rray_open [prf, in mathcomp.analysis.topology_theory.order_topology]
Rreal_axiom [prf, in mathcomp.reals_stdlib.Rstruct]
Rreal_closed_axiom [prf, in mathcomp.reals_stdlib.Rstruct]
RsqrtE [prf, in mathcomp.reals_stdlib.Rstruct]
Rstruct [file, in mathcomp.reals_stdlib.Rstruct]
Rstruct_topology [file, in mathcomp.analysis_stdlib.Rstruct_topology]
Rsup_isLub [prf, in mathcomp.reals_stdlib.Rstruct]
Rsup_ub [prf, in mathcomp.reals_stdlib.Rstruct]
Rsupremums_neq0 [prf, in mathcomp.reals_stdlib.Rstruct]
rsval [proj, in mathcomp.experimental_reals.discrete]
rsvalP [proj, in mathcomp.experimental_reals.discrete]
rT [abbrev, in mathcomp.analysis.measure]
rT [abbrev, in mathcomp.analysis.measure]
Rtoint [def, in mathcomp.reals.reals]
RtointK [prf, in mathcomp.reals.reals]
RtointN [prf, in mathcomp.reals.reals]
Rtointn [prf, in mathcomp.reals.reals]
Rtointz [prf, in mathcomp.reals.reals]
runpickle [def, in mathcomp.experimental_reals.discrete]
rV_compact [prf, in mathcomp.analysis.normedtype]