P (Abbreviations)
| 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 | _ |
| Notations |
P (Abbreviations)
Path [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]Path.clone [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.copy [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.Exports.pathType [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.on [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.on_ [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
ph [abbrev, in mathcomp.classical.wochoice]
ph [abbrev, in mathcomp.classical.filter]
PhantomF [abbrev, in mathcomp.analysis.landau]
PhantomF [abbrev, in mathcomp.analysis.landau]
PhantomF [abbrev, in mathcomp.analysis.landau]
pinv [abbrev, in mathcomp.classical.functions]
pinv [abbrev, in mathcomp.classical.functions]
Pointed [abbrev, in mathcomp.classical.classical_sets]
Pointed.clone [abbrev, in mathcomp.classical.classical_sets]
Pointed.copy [abbrev, in mathcomp.classical.classical_sets]
Pointed.Exports.pointedType [abbrev, in mathcomp.classical.classical_sets]
Pointed.on [abbrev, in mathcomp.classical.classical_sets]
Pointed.on_ [abbrev, in mathcomp.classical.classical_sets]
PointedDiscreteOrderTopology [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.Exports.pdiscreteOrderTopologicalType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.Exports.pdiscreteTopologicalType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedFiltered [abbrev, in mathcomp.classical.filter]
PointedFiltered.clone [abbrev, in mathcomp.classical.filter]
PointedFiltered.copy [abbrev, in mathcomp.classical.filter]
PointedFiltered.Exports.pfilteredType [abbrev, in mathcomp.classical.filter]
PointedFiltered.on [abbrev, in mathcomp.classical.filter]
PointedFiltered.on_ [abbrev, in mathcomp.classical.filter]
PointedNbhs [abbrev, in mathcomp.classical.filter]
PointedNbhs.clone [abbrev, in mathcomp.classical.filter]
PointedNbhs.copy [abbrev, in mathcomp.classical.filter]
PointedNbhs.Exports.pnbhsType [abbrev, in mathcomp.classical.filter]
PointedNbhs.on [abbrev, in mathcomp.classical.filter]
PointedNbhs.on_ [abbrev, in mathcomp.classical.filter]
PointedTopological [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.clone [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.copy [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.Exports.ptopologicalType [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.on [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.on_ [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedUniform [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.clone [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.copy [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.Exports.puniformType [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.on [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.on_ [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
poisson [abbrev, in mathcomp.analysis.probability]
pPbij [abbrev, in mathcomp.classical.functions]
pPinj [abbrev, in mathcomp.classical.functions]
pr_dlet [abbrev, in mathcomp.experimental_reals.distr]
pred_set [abbrev, in mathcomp.classical.classical_sets]
preimage_class [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
preimage_class_measurable_fun [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
preimage_classes [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
preimage_classes_comp [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
preimage_itv_c_infty [abbrev, in mathcomp.classical.classical_sets]
preimage_itv_infty_c [abbrev, in mathcomp.classical.classical_sets]
preimage_itv_infty_o [abbrev, in mathcomp.classical.classical_sets]
preimage_itv_o_infty [abbrev, in mathcomp.classical.classical_sets]
PreTopologicalLmod_isTvs [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmod_isTvs.axioms [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmod_isTvs.Build [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmodule [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmodule.clone [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmodule.copy [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmodule.Exports.preTopologicalLmodType [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmodule.on [abbrev, in mathcomp.analysis.tvs]
PreTopologicalLmodule.on_ [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule.clone [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule.copy [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule.on [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule.on_ [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule_isTopologicalNmodule [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule_isTopologicalNmodule.axioms [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule_isTopologicalNmodule.Build [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule_isTopologicalZmodule [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule_isTopologicalZmodule.axioms [abbrev, in mathcomp.analysis.tvs]
PreTopologicalNmodule_isTopologicalZmodule.Build [abbrev, in mathcomp.analysis.tvs]
PreTopologicalZmodule [abbrev, in mathcomp.analysis.tvs]
PreTopologicalZmodule.clone [abbrev, in mathcomp.analysis.tvs]
PreTopologicalZmodule.copy [abbrev, in mathcomp.analysis.tvs]
PreTopologicalZmodule.on [abbrev, in mathcomp.analysis.tvs]
PreTopologicalZmodule.on_ [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule.clone [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule.copy [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule.on [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule.on_ [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule_isUniformLmodule [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule_isUniformLmodule.axioms [abbrev, in mathcomp.analysis.tvs]
PreUniformLmodule_isUniformLmodule.Build [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule.clone [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule.copy [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule.on [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule.on_ [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule_isUniformNmodule [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule_isUniformNmodule.axioms [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule_isUniformNmodule.Build [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule_isUniformZmodule [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule_isUniformZmodule.axioms [abbrev, in mathcomp.analysis.tvs]
PreUniformNmodule_isUniformZmodule.Build [abbrev, in mathcomp.analysis.tvs]
PreUniformZmodule [abbrev, in mathcomp.analysis.tvs]
PreUniformZmodule.clone [abbrev, in mathcomp.analysis.tvs]
PreUniformZmodule.copy [abbrev, in mathcomp.analysis.tvs]
PreUniformZmodule.on [abbrev, in mathcomp.analysis.tvs]
PreUniformZmodule.on_ [abbrev, in mathcomp.analysis.tvs]
pro1 [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
pro2 [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
Probability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.clone [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.copy [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.Exports.probability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.on [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.on_ [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
ProbabilityKernel [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.clone [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.copy [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.Exports.probability_kernel [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.on [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.on_ [abbrev, in mathcomp.analysis.kernel]
prod_measurable_funP [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
prod_open [abbrev, in mathcomp.analysis.function_spaces]
prop_of [abbrev, in mathcomp.classical.filter]
PseudoMetric [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.clone [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.copy [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.Exports.pseudoMetricType [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.on [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.on_ [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
pseudoMetric_from_normedZmodType.T [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.Exports.pseudoMetricNormedZmodType [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod_Lmodule_isNormedModule [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Lmodule_isNormedModule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Tvs_isNormedModule [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Tvs_isNormedModule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Tvs_isNormedModule.Build [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoPointedMetric [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.clone [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.copy [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.Exports.pseudoPMetricType [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.on [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.on_ [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
psumB [abbrev, in mathcomp.experimental_reals.realsum]