'P' (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 | _ | * |
P (Lemmas)
padde_eq0 [prf, in mathcomp.analysis.constructive_ereal]pair_fsbig [prf, in mathcomp.classical.fsbigop]
parameterized_integral_continuous [prf, in mathcomp.analysis.ftc]
parameterized_integral_cvg_at_left [prf, in mathcomp.analysis.ftc]
parameterized_integral_cvg_left [prf, in mathcomp.analysis.ftc]
parameterized_integral_near_left [prf, in mathcomp.analysis.ftc]
patch_indic [prf, in mathcomp.analysis.numfun]
patch_inj_subproof [prf, in mathcomp.classical.functions]
patch_pred [prf, in mathcomp.classical.functions]
patch_set0 [prf, in mathcomp.classical.functions]
patch_setI [prf, in mathcomp.classical.functions]
patch_setT [prf, in mathcomp.classical.functions]
patchC [prf, in mathcomp.classical.functions]
patchE [prf, in mathcomp.classical.functions]
patchN [prf, in mathcomp.classical.functions]
patchT [prf, in mathcomp.classical.functions]
path_lt_filter0 [prf, in mathcomp.classical.mathcomp_extra]
path_lt_filterT [prf, in mathcomp.classical.mathcomp_extra]
path_lt_head [prf, in mathcomp.classical.mathcomp_extra]
path_lt_last_filter [prf, in mathcomp.classical.mathcomp_extra]
path_lt_le_last [prf, in mathcomp.classical.mathcomp_extra]
Pbij [prf, in mathcomp.classical.functions]
PbijTT [prf, in mathcomp.classical.functions]
pcard_eq [prf, in mathcomp.classical.cardinality]
pcard_eqP [prf, in mathcomp.classical.cardinality]
pcard_geP [prf, in mathcomp.classical.cardinality]
pcard_injP [prf, in mathcomp.classical.cardinality]
pcard_leP [prf, in mathcomp.classical.cardinality]
pcard_leTP [prf, in mathcomp.classical.cardinality]
pcard_surjP [prf, in mathcomp.classical.cardinality]
Pchoice [prf, in mathcomp.classical.boolp]
Pcountable [prf, in mathcomp.classical.cardinality]
Peq [prf, in mathcomp.classical.boolp]
perfect_diagonal [prf, in mathcomp.analysis.function_spaces]
perfect_prod [prf, in mathcomp.analysis.function_spaces]
perfect_set2 [prf, in mathcomp.analysis.topology]
perfectTP [prf, in mathcomp.analysis.topology]
periodicn [prf, in mathcomp.analysis.trigo]
perm_eq_trivIset [prf, in mathcomp.classical.classical_sets]
pexpR_gt1 [prf, in mathcomp.analysis.exp]
pfcard_geP [prf, in mathcomp.classical.cardinality]
pfsume_eq0 [prf, in mathcomp.analysis.ereal]
pfsumr_eq0 [prf, in mathcomp.classical.fsbigop]
Pfun [prf, in mathcomp.classical.functions]
pi_continuous [prf, in mathcomp.analysis.topology]
pi_ge0 [prf, in mathcomp.analysis.trigo]
pi_ge2 [prf, in mathcomp.analysis.trigo]
pi_gt0 [prf, in mathcomp.analysis.trigo]
pickR_ex [prf, in mathcomp.analysis.Rstruct]
pickR_ext [prf, in mathcomp.analysis.Rstruct]
pickR_some [prf, in mathcomp.analysis.Rstruct]
pigeonhole [prf, in mathcomp.classical.cardinality]
pihalf_02 [prf, in mathcomp.analysis.trigo]
pihalf_02_cos_pihalf [prf, in mathcomp.analysis.trigo]
pihalf_ge1 [prf, in mathcomp.analysis.trigo]
pihalf_lt2 [prf, in mathcomp.analysis.trigo]
pihalfE [prf, in mathcomp.analysis.trigo]
pinfty_ex_ge [prf, in mathcomp.analysis.normedtype]
pinfty_ex_gt [prf, in mathcomp.analysis.normedtype]
pinfty_ex_gt0 [prf, in mathcomp.analysis.normedtype]
pinfty_snum_subproof [prf, in mathcomp.analysis.constructive_ereal]
pinfty_wlength_itv [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
Pinj [prf, in mathcomp.classical.functions]
pinvK [prf, in mathcomp.classical.functions]
pinvKV [prf, in mathcomp.classical.functions]
pmule_lge0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_lgt0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_lle0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_llt0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_rge0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_rgt0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_rle0 [prf, in mathcomp.analysis.constructive_ereal]
pmule_rlt0 [prf, in mathcomp.analysis.constructive_ereal]
point_uniform_separator [prf, in mathcomp.analysis.normedtype]
pointwise_almost_uniform [prf, in mathcomp.analysis.lebesgue_measure]
pointwise_compact_closure [prf, in mathcomp.analysis.function_spaces]
pointwise_compact_cvg [prf, in mathcomp.analysis.function_spaces]
pointwise_cvg_compact_family [prf, in mathcomp.analysis.function_spaces]
pointwise_cvg_entourage [prf, in mathcomp.analysis.function_spaces]
pointwise_cvg_family_singleton [prf, in mathcomp.analysis.function_spaces]
pointwise_cvgE [prf, in mathcomp.analysis.function_spaces]
pointwise_cvgP [prf, in mathcomp.analysis.function_spaces]
pointwise_precompact_equicontinuous [prf, in mathcomp.analysis.function_spaces]
pointwise_precompact_precompact [prf, in mathcomp.analysis.function_spaces]
pointwise_precompact_subset [prf, in mathcomp.analysis.function_spaces]
pointwise_uniform_cvg [prf, in mathcomp.analysis.function_spaces]
Pos_to_natE [prf, in mathcomp.classical.mathcomp_extra]
posE [prf, in mathcomp.analysis.signed]
positive_negative0 [prf, in mathcomp.analysis.charge]
posnum_subdef [prf, in mathcomp.analysis.signed]
posnumeP [prf, in mathcomp.analysis.constructive_ereal]
posnumP [prf, in mathcomp.analysis.signed]
Posz_snum_subproof [prf, in mathcomp.analysis.signed]
poweR0r [prf, in mathcomp.analysis.exp]
poweR12_sqrt [prf, in mathcomp.analysis.exp]
poweR1r [prf, in mathcomp.analysis.exp]
poweR_EFin [prf, in mathcomp.analysis.exp]
poweR_eq0 [prf, in mathcomp.analysis.exp]
poweR_eq0_eq0 [prf, in mathcomp.analysis.exp]
poweR_eqy [prf, in mathcomp.analysis.exp]
poweR_ge0 [prf, in mathcomp.analysis.exp]
poweR_gt0 [prf, in mathcomp.analysis.exp]
poweR_lty [prf, in mathcomp.analysis.exp]
poweRAC [prf, in mathcomp.analysis.exp]
poweRB [prf, in mathcomp.analysis.exp]
poweRB_defE [prf, in mathcomp.analysis.exp]
poweRD [prf, in mathcomp.analysis.exp]
poweRD_defE [prf, in mathcomp.analysis.exp]
poweRe0 [prf, in mathcomp.analysis.exp]
poweRe1 [prf, in mathcomp.analysis.exp]
poweRM [prf, in mathcomp.analysis.exp]
poweRN [prf, in mathcomp.analysis.exp]
poweRNyr [prf, in mathcomp.analysis.exp]
poweRrM [prf, in mathcomp.analysis.exp]
powerset_filter_fromP [prf, in mathcomp.analysis.topology]
powerset_lambda_system [prf, in mathcomp.analysis.measure]
powerset_sigma_ring [prf, in mathcomp.analysis.measure]
poweRyr [prf, in mathcomp.analysis.exp]
powR0 [prf, in mathcomp.analysis.exp]
powR1 [prf, in mathcomp.analysis.exp]
powR12_sqrt [prf, in mathcomp.analysis.exp]
powR_eq0 [prf, in mathcomp.analysis.exp]
powR_eq0_eq0 [prf, in mathcomp.analysis.exp]
powR_ge0 [prf, in mathcomp.analysis.exp]
powR_gt0 [prf, in mathcomp.analysis.exp]
powR_injective [prf, in mathcomp.analysis.exp]
powR_intmul [prf, in mathcomp.analysis.exp]
powR_inv1 [prf, in mathcomp.analysis.exp]
powR_invn [prf, in mathcomp.analysis.exp]
powR_Lnorm [prf, in mathcomp.analysis.hoelder]
powR_mulrn [prf, in mathcomp.analysis.exp]
powRAC [prf, in mathcomp.analysis.exp]
powRB [prf, in mathcomp.analysis.exp]
powRD [prf, in mathcomp.analysis.exp]
powRM [prf, in mathcomp.analysis.exp]
powRN [prf, in mathcomp.analysis.exp]
powRr0 [prf, in mathcomp.analysis.exp]
powRr1 [prf, in mathcomp.analysis.exp]
powRrM [prf, in mathcomp.analysis.exp]
pPbij_ [prf, in mathcomp.classical.functions]
ppcard_eqP [prf, in mathcomp.classical.cardinality]
ppcard_leP [prf, in mathcomp.classical.cardinality]
pPinj_ [prf, in mathcomp.classical.functions]
Ppointed [prf, in mathcomp.classical.classical_sets]
precompact_closed [prf, in mathcomp.analysis.topology]
precompact_equicontinuous [prf, in mathcomp.analysis.function_spaces]
precompact_pointwise_precompact [prf, in mathcomp.analysis.function_spaces]
precompact_subset [prf, in mathcomp.analysis.topology]
precompactE [prf, in mathcomp.analysis.topology]
pred0pP [prf, in mathcomp.classical.boolp]
pred_oapp_set [prf, in mathcomp.classical.classical_sets]
pred_oappE [prf, in mathcomp.classical.classical_sets]
predeq2E [prf, in mathcomp.classical.boolp]
predeq2P [prf, in mathcomp.classical.boolp]
predeq3E [prf, in mathcomp.classical.boolp]
predeq3P [prf, in mathcomp.classical.boolp]
predeqE [prf, in mathcomp.classical.boolp]
predeqP [prf, in mathcomp.classical.boolp]
preimage0 [prf, in mathcomp.classical.classical_sets]
preimage0eq [prf, in mathcomp.classical.classical_sets]
preimage10 [prf, in mathcomp.classical.classical_sets]
preimage10P [prf, in mathcomp.classical.classical_sets]
preimage_abse_ninfty [prf, in mathcomp.analysis.ereal]
preimage_abse_pinfty [prf, in mathcomp.analysis.ereal]
preimage_add [prf, in mathcomp.analysis.lebesgue_integral]
preimage_bigcap [prf, in mathcomp.classical.classical_sets]
preimage_bigcup [prf, in mathcomp.classical.classical_sets]
preimage_class_measurable_fun [prf, in mathcomp.analysis.measure]
preimage_classes_comp [prf, in mathcomp.analysis.measure]
preimage_comp [prf, in mathcomp.classical.classical_sets]
preimage_cst [prf, in mathcomp.classical.functions]
preimage_cstM [prf, in mathcomp.analysis.lebesgue_integral]
preimage_EFin_setT [prf, in mathcomp.analysis.lebesgue_measure]
preimage_false [prf, in mathcomp.classical.classical_sets]
preimage_id [prf, in mathcomp.classical.classical_sets]
preimage_image [prf, in mathcomp.classical.classical_sets]
preimage_indic [prf, in mathcomp.analysis.numfun]
preimage_itv [prf, in mathcomp.classical.classical_sets]
preimage_itv_c_infty [prf, in mathcomp.classical.classical_sets]
preimage_itv_infty_c [prf, in mathcomp.classical.classical_sets]
preimage_itv_infty_o [prf, in mathcomp.classical.classical_sets]
preimage_itv_o_infty [prf, in mathcomp.classical.classical_sets]
preimage_mem_false [prf, in mathcomp.classical.classical_sets]
preimage_mem_true [prf, in mathcomp.classical.classical_sets]
preimage_nnfun0 [prf, in mathcomp.analysis.lebesgue_integral]
preimage_range [prf, in mathcomp.classical.classical_sets]
preimage_restrict [prf, in mathcomp.classical.functions]
preimage_set0 [prf, in mathcomp.classical.classical_sets]
preimage_setC [prf, in mathcomp.classical.classical_sets]
preimage_setI [prf, in mathcomp.classical.classical_sets]
preimage_setI_eq0 [prf, in mathcomp.classical.classical_sets]
preimage_setT [prf, in mathcomp.classical.classical_sets]
preimage_setU [prf, in mathcomp.classical.classical_sets]
preimage_subset [prf, in mathcomp.classical.classical_sets]
preimage_true [prf, in mathcomp.classical.classical_sets]
preimageEinv [prf, in mathcomp.classical.functions]
preimageEoinv [prf, in mathcomp.classical.functions]
principal_filter_proper [prf, in mathcomp.analysis.topology]
principal_filter_ultra [prf, in mathcomp.analysis.topology]
principal_filterP [prf, in mathcomp.analysis.topology]
probability_distribution [prf, in mathcomp.analysis.probability]
probability_le1 [prf, in mathcomp.analysis.measure]
probability_range [prf, in mathcomp.analysis.probability]
probability_setC [prf, in mathcomp.analysis.measure]
prod_ball_center [prf, in mathcomp.analysis.topology]
prod_ball_sym [prf, in mathcomp.analysis.topology]
prod_ball_triangle [prf, in mathcomp.analysis.topology]
prod_ent_filter [prf, in mathcomp.analysis.topology]
prod_ent_inv [prf, in mathcomp.analysis.topology]
prod_ent_nbhsE [prf, in mathcomp.analysis.topology]
prod_ent_refl [prf, in mathcomp.analysis.topology]
prod_ent_split [prf, in mathcomp.analysis.topology]
prod_entourage [prf, in mathcomp.analysis.topology]
prod_entP [prf, in mathcomp.analysis.topology]
prod_measurable_funP [prf, in mathcomp.analysis.measure]
prod_nbhs_filter [prf, in mathcomp.analysis.topology]
prod_nbhs_nbhs [prf, in mathcomp.analysis.topology]
prod_nbhs_singleton [prf, in mathcomp.analysis.topology]
prod_norm_ball [prf, in mathcomp.analysis.normedtype]
prod_norm_scale [prf, in mathcomp.analysis.normedtype]
ProdNormedZmodule.norm_eq0 [prf, in mathcomp.analysis.prodnormedzmodule]
ProdNormedZmodule.normD [prf, in mathcomp.analysis.prodnormedzmodule]
ProdNormedZmodule.normMn [prf, in mathcomp.analysis.prodnormedzmodule]
ProdNormedZmodule.normrN [prf, in mathcomp.analysis.prodnormedzmodule]
ProdNormedZmodule.prod_normE [prf, in mathcomp.analysis.prodnormedzmodule]
product_measure1E [prf, in mathcomp.analysis.lebesgue_integral]
product_measure2E [prf, in mathcomp.analysis.lebesgue_integral]
product_measure_unique [prf, in mathcomp.analysis.lebesgue_integral]
proj_continuous [prf, in mathcomp.analysis.function_spaces]
proj_open [prf, in mathcomp.analysis.function_spaces]
projK [prf, in mathcomp.classical.mathcomp_extra]
Prop_irrelevance [prf, in mathcomp.classical.boolp]
prop_ofP [prf, in mathcomp.analysis.topology]
PropB [prf, in mathcomp.classical.boolp]
propeqE [prf, in mathcomp.classical.boolp]
propeqP [prf, in mathcomp.classical.boolp]
proper_image [prf, in mathcomp.analysis.topology]
proper_meetsxx [prf, in mathcomp.analysis.topology]
properEneq [prf, in mathcomp.classical.classical_sets]
properW [prf, in mathcomp.classical.classical_sets]
properxx [prf, in mathcomp.classical.classical_sets]
propext [prf, in mathcomp.classical.boolp]
propF [prf, in mathcomp.classical.boolp]
PropInFilter.tE [prf, in mathcomp.analysis.topology]
propT [prf, in mathcomp.classical.boolp]
ps_inftyP [prf, in mathcomp.analysis.lebesgue_measure]
pselect [prf, in mathcomp.classical.boolp]
pselectT [prf, in mathcomp.classical.boolp]
pseries_diffs_equiv [prf, in mathcomp.analysis.exp]
pseries_diffs_inv_fact [prf, in mathcomp.analysis.exp]
pseries_diffs_sumE [prf, in mathcomp.analysis.exp]
pseries_diffsN [prf, in mathcomp.analysis.exp]
pseries_snd_diffs [prf, in mathcomp.analysis.exp]
pseudometric_normal [prf, in mathcomp.analysis.normedtype]
pseudoMetricNormedZModType_hausdorff [prf, in mathcomp.analysis.normedtype]
Psplitinj [prf, in mathcomp.classical.functions]
PsplitinjT [prf, in mathcomp.classical.functions]
PsplitsurjT [prf, in mathcomp.classical.functions]
Psurj [prf, in mathcomp.classical.functions]
punct_eitv_bndy [prf, in mathcomp.analysis.lebesgue_measure]
punct_eitv_Nybnd [prf, in mathcomp.analysis.lebesgue_measure]
punct_eitv_setTL [prf, in mathcomp.analysis.lebesgue_measure]
punct_eitv_setTR [prf, in mathcomp.analysis.lebesgue_measure]