M (Definitions)
| 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 |
M (Definitions)
map_itv [def, in mathcomp.reals.interval_inference]map_itv_bound [def, in mathcomp.reals.interval_inference]
map_pair [def, in mathcomp.classical.unstable]
matrix_triangle [def, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
max_g2 [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence]
max_g2' [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence]
max_mfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
max_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
max_nonzero_subdef [def, in mathcomp.reals.signed]
max_reality_subdef [def, in mathcomp.reals.signed]
max_sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
max_snum [def, in mathcomp.reals.signed]
maximal [def, in mathcomp.classical.wochoice]
maximal_disjoint_subcollection [def, in mathcomp.classical.classical_sets]
maximum_of [def, in mathcomp.classical.wochoice]
maxn_snum [def, in mathcomp.reals.signed]
measurable [def, in mathcomp.analysis.measure]
Measurable.Exports.join_measure_Measurable_between_measure_AlgebraOfSets_and_measure_SigmaRing [def, in mathcomp.analysis.measure]
Measurable.pack_ [def, in mathcomp.analysis.measure]
Measurable.phant_clone [def, in mathcomp.analysis.measure]
Measurable.phant_on_ [def, in mathcomp.analysis.measure]
measurable0 [def, in mathcomp.analysis.measure]
measurable_cover [def, in mathcomp.analysis.measure]
measurable_fun [def, in mathcomp.analysis.measure]
measurable_funPT [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
measurable_kernel [def, in mathcomp.analysis.kernel]
measurable_subset_sigma_subadditive [def, in mathcomp.analysis.measure]
MeasurableFun.pack_ [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
MeasurableFun.phant_clone [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
MeasurableFun.phant_on_ [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
MeasurableFun_isDiscrete.identity_builder [def, in mathcomp.analysis.probability]
MeasurableFun_isDiscrete.phant_axioms [def, in mathcomp.analysis.probability]
MeasurableFun_isDiscrete.phant_Build [def, in mathcomp.analysis.probability]
measurableI [def, in mathcomp.analysis.measure]
measurableR [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
measurableT [def, in mathcomp.analysis.measure]
measurableTypeR [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
measurableU [def, in mathcomp.analysis.measure]
Measure.pack_ [def, in mathcomp.analysis.measure]
Measure.phant_clone [def, in mathcomp.analysis.measure]
Measure.phant_on_ [def, in mathcomp.analysis.measure]
measure_add [def, in mathcomp.analysis.measure]
measure_dominates [def, in mathcomp.analysis.measure]
measure_extension [def, in mathcomp.analysis.measure]
measure_fam_uub [def, in mathcomp.analysis.kernel]
measure_ge0 [def, in mathcomp.analysis.measure]
measure_inum [def, in mathcomp.analysis.measure]
measure_is_complete [def, in mathcomp.analysis.measure]
Measure_isFinite.phant_axioms [def, in mathcomp.analysis.measure]
Measure_isFinite.phant_Build [def, in mathcomp.analysis.measure]
Measure_isProbability.phant_axioms [def, in mathcomp.analysis.measure]
Measure_isProbability.phant_Build [def, in mathcomp.analysis.measure]
Measure_isSFinite.phant_axioms [def, in mathcomp.analysis.measure]
Measure_isSFinite.phant_Build [def, in mathcomp.analysis.measure]
Measure_isSigmaFinite.phant_axioms [def, in mathcomp.analysis.measure]
Measure_isSigmaFinite.phant_Build [def, in mathcomp.analysis.measure]
Measure_isSubProbability.phant_axioms [def, in mathcomp.analysis.measure]
Measure_isSubProbability.phant_Build [def, in mathcomp.analysis.measure]
measure_of_charge [def, in mathcomp.analysis.charge]
measure_prod_display [def, in mathcomp.analysis.measure]
measure_semi_additive [def, in mathcomp.analysis.measure]
measure_semi_sigma_additive [def, in mathcomp.analysis.measure]
measure_tuple_display [def, in mathcomp.analysis.measure]
measure_uub [def, in mathcomp.analysis.kernel]
meets [def, in mathcomp.classical.classical_sets]
mem_fun [def, in mathcomp.classical.functions]
metric_discrete [def, in mathcomp.analysis.topology_theory.discrete_topology]
mflip [def, in mathcomp.experimental_reals.distr]
mfrestr [def, in mathcomp.analysis.measure]
mfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
mfun_key [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
mfun_keyed [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
mfun_Sub [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
min_nonzero_subdef [def, in mathcomp.reals.signed]
min_reality_subdef [def, in mathcomp.reals.signed]
min_snum [def, in mathcomp.reals.signed]
mindic [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
minimal [def, in mathcomp.classical.wochoice]
minimum_of [def, in mathcomp.classical.wochoice]
minn_snum [def, in mathcomp.reals.signed]
mk_path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
mk_sequence [def, in mathcomp.analysis.sequences]
mkcomp [def, in mathcomp.analysis.kernel]
mkcomp_noparam [def, in mathcomp.analysis.kernel]
mkcts [def, in mathcomp.analysis.topology_theory.topology_structure]
mkdistr [def, in mathcomp.experimental_reals.distr]
mkdistrd [def, in mathcomp.experimental_reals.distr]
mkfun [def, in mathcomp.classical.functions]
mkfun_fun [def, in mathcomp.classical.functions]
mkproduct [def, in mathcomp.analysis.kernel]
mkset [def, in mathcomp.classical.classical_sets]
mlet [def, in mathcomp.experimental_reals.distr]
mlim [def, in mathcomp.experimental_reals.distr]
mmt_gen_fun [def, in mathcomp.analysis.probability]
mnormalize [def, in mathcomp.analysis.measure]
mnull [def, in mathcomp.experimental_reals.distr]
monotone [def, in mathcomp.analysis.measure]
monotonous [def, in mathcomp.classical.unstable]
mrat [def, in mathcomp.experimental_reals.distr]
mrestr [def, in mathcomp.experimental_reals.distr]
mrestr [def, in mathcomp.analysis.measure]
mscale [def, in mathcomp.analysis.measure]
mseries [def, in mathcomp.analysis.measure]
mset [def, in mathcomp.analysis.measure]
msum [def, in mathcomp.analysis.measure]
mu_ext [def, in mathcomp.analysis.measure]
mul_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
mul_nonzero_subdef [def, in mathcomp.reals.signed]
mul_reality_subdef [def, in mathcomp.reals.signed]
mul_snum [def, in mathcomp.reals.signed]
mule [def, in mathcomp.reals.constructive_ereal]
mule_def [def, in mathcomp.reals.constructive_ereal]
mule_defE [def, in mathcomp.reals.constructive_ereal]
muln_snum [def, in mathcomp.reals.signed]
mulr_infty [def, in mathcomp.reals.constructive_ereal]
mx_ball [def, in mathcomp.analysis.topology_theory.matrix_topology]
mx_ent [def, in mathcomp.analysis.topology_theory.matrix_topology]
mx_norm [def, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
mzero [def, in mathcomp.analysis.measure]