'R' (Lemmas)
| 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 (Lemmas)
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_idomainMixin [prf, in mathcomp.reals_stdlib.Rstruct]
R_total [prf, in mathcomp.reals_stdlib.Rstruct]
rad_ker [prf, in mathcomp.analysis.forms]
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_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.chain_rule [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.change_of_variables [prf, 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]
Radon_NikodymE [prf, in mathcomp.analysis.charge]
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]
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_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_subproof [prf, in mathcomp.reals.signed]
real_field_typ_subproof [prf, in mathcomp.reals.signed]
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_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_sup_adherent [prf, in mathcomp.reals_stdlib.Rstruct]
realDe [prf, in mathcomp.reals.constructive_ereal]
realMe [prf, in mathcomp.reals.constructive_ereal]
reflect_eq [prf, in mathcomp.classical.boolp]
regular_openP [prf, in mathcomp.analysis.normedtype]
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_psum [prf, in mathcomp.experimental_reals.realsum]
reindex_psum_onto [prf, in mathcomp.experimental_reals.realsum]
repr_comp_continuous [prf, in mathcomp.analysis.topology_theory.quotient_topology]
Req_EM_T [prf, in mathcomp.reals_stdlib.Rstruct]
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]
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]
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.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.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.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]
Rhausdorff [prf, in mathcomp.analysis.separation_axioms]
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_gt0 [prf, in mathcomp.analysis.exp]
right_bounded_interior [prf, in mathcomp.analysis.normedtype]
right_continuousW [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
ring_semi_sigma_additive [prf, in mathcomp.analysis.measure]
ring_sigma_subadditive [prf, in mathcomp.analysis.measure]
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_subring_closed [prf, in mathcomp.reals.reals]
RintC [prf, in mathcomp.reals.reals]
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]
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_out [prf, in mathcomp.reals_stdlib.Rstruct]
RinvxRmult [prf, 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 [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_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]
RoppE [prf, in mathcomp.reals_stdlib.Rstruct]
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]
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]
Rsup_isLub [prf, in mathcomp.reals_stdlib.Rstruct]
Rsup_ub [prf, in mathcomp.reals_stdlib.Rstruct]
Rsupremums_neq0 [prf, in mathcomp.reals_stdlib.Rstruct]
RtointK [prf, in mathcomp.reals.reals]
RtointN [prf, in mathcomp.reals.reals]
Rtointn [prf, in mathcomp.reals.reals]
Rtointz [prf, in mathcomp.reals.reals]
rV_compact [prf, in mathcomp.analysis.normedtype]