'P' (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

P (Lemmas)

padde_eq0 [prf, in mathcomp.reals.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]
partition_disjoint_bigfcup [prf, in mathcomp.classical.mathcomp_extra]
partition_psum [prf, in mathcomp.experimental_reals.realsum]
partition_psum_cond [prf, in mathcomp.experimental_reals.realsum]
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_eqP [prf, in mathcomp.analysis.homotopy_theory.continuous_path]
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]
perfectTP [prf, in mathcomp.analysis.separation_axioms]
perfectTP_ex [prf, in mathcomp.analysis.separation_axioms]
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_theory.quotient_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.reals_stdlib.Rstruct]
pickR_ext [prf, in mathcomp.reals_stdlib.Rstruct]
pickR_some [prf, in mathcomp.reals_stdlib.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.reals.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.reals.constructive_ereal]
pmule_lgt0 [prf, in mathcomp.reals.constructive_ereal]
pmule_lle0 [prf, in mathcomp.reals.constructive_ereal]
pmule_llt0 [prf, in mathcomp.reals.constructive_ereal]
pmule_rge0 [prf, in mathcomp.reals.constructive_ereal]
pmule_rgt0 [prf, in mathcomp.reals.constructive_ereal]
pmule_rle0 [prf, in mathcomp.reals.constructive_ereal]
pmule_rlt0 [prf, in mathcomp.reals.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.reals.signed]
positive_negative0 [prf, in mathcomp.analysis.charge]
posnum_subdef [prf, in mathcomp.reals.signed]
posnumeP [prf, in mathcomp.reals.constructive_ereal]
posnumP [prf, in mathcomp.reals.signed]
Posz_snum_subproof [prf, in mathcomp.reals.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.classical.filter]
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]
pr_and [prf, in mathcomp.experimental_reals.distr]
pr_bigor_indep [prf, in mathcomp.experimental_reals.distr]
pr_dmargin [prf, in mathcomp.experimental_reals.distr]
pr_dunit [prf, in mathcomp.experimental_reals.distr]
pr_eq0 [prf, in mathcomp.experimental_reals.distr]
pr_exp [prf, in mathcomp.experimental_reals.distr]
pr_mem [prf, in mathcomp.experimental_reals.distr]
pr_mem_map [prf, in mathcomp.experimental_reals.distr]
pr_or [prf, in mathcomp.experimental_reals.distr]
pr_or_indep [prf, in mathcomp.experimental_reals.distr]
pr_pred0 [prf, in mathcomp.experimental_reals.distr]
pr_pred0_eq [prf, in mathcomp.experimental_reals.distr]
pr_pred1 [prf, in mathcomp.experimental_reals.distr]
pr_predC [prf, in mathcomp.experimental_reals.distr]
pr_predT [prf, in mathcomp.experimental_reals.distr]
pr_split [prf, in mathcomp.experimental_reals.distr]
prc_sum [prf, in mathcomp.experimental_reals.distr]
precompact_closed [prf, in mathcomp.analysis.topology_theory.compact]
precompact_equicontinuous [prf, in mathcomp.analysis.function_spaces]
precompact_pointwise_precompact [prf, in mathcomp.analysis.function_spaces]
precompact_subset [prf, in mathcomp.analysis.topology_theory.compact]
precompactE [prf, in mathcomp.analysis.topology_theory.compact]
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_itvcy [prf, in mathcomp.classical.classical_sets]
preimage_itvNyc [prf, in mathcomp.classical.classical_sets]
preimage_itvNyo [prf, in mathcomp.classical.classical_sets]
preimage_itvoy [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]
prID [prf, in mathcomp.experimental_reals.distr]
principal_filter_proper [prf, in mathcomp.classical.filter]
principal_filter_ultra [prf, in mathcomp.classical.filter]
principal_filterP [prf, in mathcomp.classical.filter]
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_add_continuous [prf, in mathcomp.analysis.tvs]
prod_ball_center [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ball_sym [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ball_triangle [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ent_filter [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ent_inv [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ent_nbhsE [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ent_refl [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_ent_split [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_entourage [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_entP [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_locally_convex [prf, in mathcomp.analysis.tvs]
prod_measurable_funP [prf, in mathcomp.analysis.measure]
prod_nbhs_filter [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_nbhs_nbhs [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_nbhs_singleton [prf, in mathcomp.analysis.topology_theory.product_topology]
prod_norm_ball [prf, in mathcomp.analysis.normedtype]
prod_norm_scale [prf, in mathcomp.analysis.normedtype]
prod_scale_continuous [prf, in mathcomp.analysis.tvs]
prodA_continuous [prf, in mathcomp.analysis.topology_theory.product_topology]
prodAK [prf, in mathcomp.classical.mathcomp_extra]
prodAr_continuous [prf, in mathcomp.analysis.topology_theory.product_topology]
prodArK [prf, in mathcomp.classical.mathcomp_extra]
prode_fin_num [prf, in mathcomp.reals.constructive_ereal]
prode_ge0 [prf, in mathcomp.reals.constructive_ereal]
ProdNormedZmodule.norm_eq0 [prf, in mathcomp.reals.prodnormedzmodule]
ProdNormedZmodule.normD [prf, in mathcomp.reals.prodnormedzmodule]
ProdNormedZmodule.normMn [prf, in mathcomp.reals.prodnormedzmodule]
ProdNormedZmodule.normrN [prf, in mathcomp.reals.prodnormedzmodule]
ProdNormedZmodule.prod_normE [prf, in mathcomp.reals.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.classical.filter]
PropB [prf, in mathcomp.classical.boolp]
propeqE [prf, in mathcomp.classical.boolp]
propeqP [prf, in mathcomp.classical.boolp]
proper_image [prf, in mathcomp.classical.filter]
proper_meetsxx [prf, in mathcomp.classical.filter]
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.classical.filter]
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]
psum0 [prf, in mathcomp.experimental_reals.realsum]
psum_abs [prf, in mathcomp.experimental_reals.realsum]
psum_absE [prf, in mathcomp.experimental_reals.realsum]
psum_as_lim [prf, in mathcomp.experimental_reals.realsum]
psum_bigop [prf, in mathcomp.experimental_reals.realsum]
psum_eq0 [prf, in mathcomp.experimental_reals.realsum]
psum_fin [prf, in mathcomp.experimental_reals.realsum]
psum_finseq [prf, in mathcomp.experimental_reals.realsum]
psum_le [prf, in mathcomp.experimental_reals.realsum]
psum_out [prf, in mathcomp.experimental_reals.realsum]
psum_pair [prf, in mathcomp.experimental_reals.realsum]
psum_pair_swap [prf, in mathcomp.experimental_reals.realsum]
psum_sum [prf, in mathcomp.experimental_reals.realsum]
psum_sup [prf, in mathcomp.experimental_reals.realsum]
psum_sup_seq [prf, in mathcomp.experimental_reals.realsum]
psumD [prf, in mathcomp.experimental_reals.realsum]
psumE [prf, in mathcomp.experimental_reals.realsum]
psumID [prf, in mathcomp.experimental_reals.realsum]
psummable_ptbounded [prf, in mathcomp.experimental_reals.realsum]
psumN [prf, in mathcomp.experimental_reals.realsum]
psumZ [prf, in mathcomp.experimental_reals.realsum]
psumZr [prf, in mathcomp.experimental_reals.realsum]
Psurj [prf, in mathcomp.classical.functions]
ptsum_homo [prf, in mathcomp.experimental_reals.realsum]
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]