C (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 |
C (Definitions)
cadd [def, in mathcomp.analysis.charge]Can.phant_axioms [def, in mathcomp.classical.functions]
Can.phant_Build [def, in mathcomp.classical.functions]
Can2.phant_axioms [def, in mathcomp.classical.functions]
Can2.phant_Build [def, in mathcomp.classical.functions]
canonical_of [def, in mathcomp.classical.boolp]
cantor_like [def, in mathcomp.analysis.cantor]
cantor_space [def, in mathcomp.analysis.cantor]
CanV.phant_axioms [def, in mathcomp.classical.functions]
CanV.phant_Build [def, in mathcomp.classical.functions]
caratheodory_display [def, in mathcomp.analysis.measure]
caratheodory_measurable [def, in mathcomp.analysis.measure]
caratheodory_type [def, in mathcomp.analysis.measure]
card_eq [def, in mathcomp.classical.cardinality]
card_le [def, in mathcomp.classical.cardinality]
cauchy [def, in mathcomp.analysis.topology_theory.uniform_structure]
cauchy_ball [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
cauchy_cvg [def, in mathcomp.analysis.topology_theory.uniform_structure]
cauchy_ex [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
cdf [def, in mathcomp.analysis.probability]
chain [def, in mathcomp.classical.wochoice]
chain_path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
Charge.pack_ [def, in mathcomp.analysis.charge]
Charge.phant_clone [def, in mathcomp.analysis.charge]
Charge.phant_on_ [def, in mathcomp.analysis.charge]
charge_of_finite_measure [def, in mathcomp.analysis.charge]
charge_semi_additive [def, in mathcomp.analysis.charge]
charge_semi_sigma_additive [def, in mathcomp.analysis.charge]
charge_variation [def, in mathcomp.analysis.charge]
Choice_isEmpty.phant_axioms [def, in mathcomp.classical.classical_sets]
Choice_isEmpty.phant_Build [def, in mathcomp.classical.classical_sets]
cjordan_neg [def, in mathcomp.analysis.charge]
cjordan_pos [def, in mathcomp.analysis.charge]
clamp [def, in mathcomp.experimental_reals.distr]
classicType [def, in mathcomp.classical.boolp]
clopen [def, in mathcomp.analysis.topology_theory.topology_structure]
close [def, in mathcomp.analysis.topology_theory.separation_axioms]
closed [def, in mathcomp.analysis.topology_theory.topology_structure]
closed_ball [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
closed_ball_ [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
closed_fam_of [def, in mathcomp.analysis.topology_theory.compact]
closure [def, in mathcomp.analysis.topology_theory.topology_structure]
cluster [def, in mathcomp.analysis.topology_theory.compact]
code [def, in mathcomp.reals.constructive_ereal]
compact [def, in mathcomp.analysis.topology_theory.compact]
compact_near [def, in mathcomp.analysis.topology_theory.compact]
compact_open [def, in mathcomp.analysis.function_spaces]
compact_open_def [def, in mathcomp.analysis.function_spaces]
compact_open_of_nbhs [def, in mathcomp.analysis.function_spaces]
compact_openK [def, in mathcomp.analysis.function_spaces]
compact_openK_nbhs [def, in mathcomp.analysis.function_spaces]
compactly_in [def, in mathcomp.analysis.function_spaces]
Complete.pack_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
Complete.phant_clone [def, in mathcomp.analysis.topology_theory.uniform_structure]
Complete.phant_on_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
completed_algebra_gen [def, in mathcomp.analysis.measurable_realfun]
completed_lebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
completed_lebesgue_stieltjes_measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
completed_measure_extension [def, in mathcomp.analysis.measure]
completely_regular_space [def, in mathcomp.analysis.normedtype_theory.urysohn]
completely_regular_uniformity.type [def, in mathcomp.analysis.normedtype_theory.urysohn]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_GRing_Lmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_GRing_Nmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_GRing_Zmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_normed_module_NormedModule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_Num_NormedZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_pseudometric_normed_Zmodule_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_NbhsLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_NbhsNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_NbhsZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_PreTopologicalLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_PreTopologicalNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_PreTopologicalZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_PreUniformLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_PreUniformNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_PreUniformZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_TopologicalLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_TopologicalNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_TopologicalZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_Tvs [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_GRing_Lmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_GRing_Nmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_GRing_Zmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_normed_module_NormedModule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_Num_NormedZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_pseudometric_normed_Zmodule_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_NbhsLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_NbhsNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_NbhsZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_PreTopologicalLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_PreTopologicalNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_PreTopologicalZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_PreUniformLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_PreUniformNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_PreUniformZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_TopologicalLmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_TopologicalNmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_TopologicalZmodule [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.Exports.join_complete_normed_module_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_Tvs [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.pack_ [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.phant_clone [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompleteNormedModule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.complete_normed_module]
CompletePseudoMetric.Exports.join_pseudometric_structure_CompletePseudoMetric_between_uniform_structure_Complete_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
CompletePseudoMetric.Exports.join_pseudometric_structure_CompletePseudoMetric_between_uniform_structure_Complete_and_pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
CompletePseudoMetric.pack_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
CompletePseudoMetric.phant_clone [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
CompletePseudoMetric.phant_on_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
connected [def, in mathcomp.analysis.topology_theory.connected]
connected_component [def, in mathcomp.analysis.topology_theory.connected]
Content.pack_ [def, in mathcomp.analysis.measure]
Content.phant_clone [def, in mathcomp.analysis.measure]
Content.phant_on_ [def, in mathcomp.analysis.measure]
content_inum [def, in mathcomp.analysis.measure]
Content_isMeasure.identity_builder [def, in mathcomp.analysis.measure]
Content_isMeasure.phant_axioms [def, in mathcomp.analysis.measure]
Content_isMeasure.phant_Build [def, in mathcomp.analysis.measure]
Content_SigmaSubAdditive_isMeasure.phant_axioms [def, in mathcomp.analysis.measure]
Content_SigmaSubAdditive_isMeasure.phant_Build [def, in mathcomp.analysis.measure]
Continuous.pack_ [def, in mathcomp.analysis.topology_theory.topology_structure]
Continuous.phant_clone [def, in mathcomp.analysis.topology_theory.topology_structure]
Continuous.phant_on_ [def, in mathcomp.analysis.topology_theory.topology_structure]
continuous_at [def, in mathcomp.classical.filter]
ContinuousFun.Exports.join_subspace_topology_ContinuousFun_between_topology_structure_Continuous_and_functions_Fun [def, in mathcomp.analysis.topology_theory.subspace_topology]
ContinuousFun.pack_ [def, in mathcomp.analysis.topology_theory.subspace_topology]
ContinuousFun.phant_clone [def, in mathcomp.analysis.topology_theory.subspace_topology]
ContinuousFun.phant_on_ [def, in mathcomp.analysis.topology_theory.subspace_topology]
contract [def, in mathcomp.reals.constructive_ereal]
contract_inj [def, in mathcomp.reals.constructive_ereal]
contraction [def, in mathcomp.analysis.normedtype_theory.normed_module]
conv [def, in mathcomp.analysis.convex]
conv1 [def, in mathcomp.analysis.convex]
convA [def, in mathcomp.analysis.convex]
convC [def, in mathcomp.analysis.convex]
convex [def, in mathcomp.analysis.tvs]
convex_function [def, in mathcomp.analysis.convex]
convex_lmodType [def, in mathcomp.analysis.convex]
convex_numDomainType [def, in mathcomp.analysis.convex]
convex_quasi_associative [def, in mathcomp.analysis.convex]
convexon [def, in mathcomp.experimental_reals.distr]
ConvexQuasiAssoc.law [def, in mathcomp.analysis.convex]
ConvexSpace.pack_ [def, in mathcomp.analysis.convex]
ConvexSpace.phant_clone [def, in mathcomp.analysis.convex]
ConvexSpace.phant_on_ [def, in mathcomp.analysis.convex]
convmm [def, in mathcomp.analysis.convex]
cos.body [def, in mathcomp.analysis.trigo]
cos.unlock [def, in mathcomp.analysis.trigo]
cos_coeff [def, in mathcomp.analysis.trigo]
cos_coeff' [def, in mathcomp.analysis.trigo]
cos_inum [def, in mathcomp.analysis.trigo]
cos_unlock_subterm [def, in mathcomp.analysis.trigo]
countable [def, in mathcomp.classical.cardinality]
countable_choiceMixin [def, in mathcomp.experimental_reals.discrete]
countable_countMixin [def, in mathcomp.experimental_reals.discrete]
countable_range [def, in mathcomp.analysis.probability]
countable_uniform.distN [def, in mathcomp.analysis.topology_theory.separation_axioms]
countable_uniform.g_ [def, in mathcomp.analysis.topology_theory.separation_axioms]
countable_uniform.n_step_ball [def, in mathcomp.analysis.topology_theory.separation_axioms]
countable_uniform.step_ball [def, in mathcomp.analysis.topology_theory.separation_axioms]
countable_uniform.type [def, in mathcomp.analysis.topology_theory.separation_axioms]
countable_uniformity [def, in mathcomp.analysis.topology_theory.uniform_structure]
counting [def, in mathcomp.analysis.measure]
covariance.body [def, in mathcomp.analysis.probability]
covariance.unlock [def, in mathcomp.analysis.probability]
covariance_unlock_subterm [def, in mathcomp.analysis.probability]
covariance_unlockable [def, in mathcomp.analysis.probability]
cover [def, in mathcomp.classical.classical_sets]
cover_compact [def, in mathcomp.analysis.topology_theory.compact]
covered_by [def, in mathcomp.analysis.measure]
cp01_clamp [def, in mathcomp.experimental_reals.distr]
cpoint [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
crestr [def, in mathcomp.analysis.charge]
crestr0 [def, in mathcomp.analysis.charge]
cscale [def, in mathcomp.analysis.charge]
cst [def, in mathcomp.classical.functions]
cst_fimfun [def, in mathcomp.classical.cardinality]
cst_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
cst_sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
cts_fun [def, in mathcomp.analysis.topology_theory.topology_structure]
Cumulative.pack_ [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
Cumulative.phant_clone [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
Cumulative.phant_on_ [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
cumulative_is_nondecreasing [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
cumulative_is_right_continuous [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
CumulativeBounded.pack_ [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
CumulativeBounded.phant_clone [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
CumulativeBounded.phant_on_ [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
cumulativeNy0 [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
cumulativey1 [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
cvg_to [def, in mathcomp.classical.filter]
cvg_to_comp_2 [def, in mathcomp.classical.filter]
cvg_toi_locally [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
cvg_toi_locally_close [def, in mathcomp.analysis.topology_theory.separation_axioms]
czero [def, in mathcomp.analysis.charge]