U (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

U

U [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
ub_ereal_sup [abbrev, in mathcomp.analysis.ereal]
ub_ereal_sup_adherent [prf, in mathcomp.analysis.ereal]
ub_lb_refl [prf, in mathcomp.classical.classical_sets]
ub_lb_set1 [prf, in mathcomp.classical.classical_sets]
ub_lb_ub [prf, in mathcomp.classical.classical_sets]
ub_lbN [prf, in mathcomp.classical.set_interval]
ub_le_sup [prf, in mathcomp.reals.reals]
ub_set1 [prf, in mathcomp.classical.classical_sets]
ubound [def, in mathcomp.classical.classical_sets]
ubound0 [prf, in mathcomp.reals.reals]
uboundT [prf, in mathcomp.analysis.ereal]
ubP [prf, in mathcomp.classical.classical_sets]
ultra_cvg_clusterE [prf, in mathcomp.analysis.topology_theory.compact]
ultra_image [prf, in mathcomp.classical.filter]
ultra_proper [proj, in mathcomp.classical.filter]
UltraFilter [rec, in mathcomp.classical.filter]
ultraFilterLemma [prf, in mathcomp.classical.filter]
unbind [def, in mathcomp.classical.functions]
uncurry_continuous [prf, in mathcomp.analysis.topology_theory.function_spaces]
uncurryK [prf, in mathcomp.classical.boolp]
unif_continuous [def, in mathcomp.analysis.topology_theory.uniform_structure]
unif_continuous_comp [prf, in mathcomp.analysis.topology_theory.uniform_structure]
unif_continuous_continuous [prf, in mathcomp.analysis.topology_theory.uniform_structure]
unif_continuousP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform [mod, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.axioms_ [rec, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.class [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.clone [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.copy [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.Exports [mod, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.Exports.uniformType [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.on [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.on_ [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.pack_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.phant_clone [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.phant_on_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.sort [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.type [rec, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
uniform_bigO [file, in mathcomp.analysis_stdlib.showcase.uniform_bigO]
uniform_bounded [def, in mathcomp.analysis.sequences]
uniform_completely_regular [prf, in mathcomp.analysis.normedtype_theory.urysohn]
uniform_discrete [def, in mathcomp.analysis.topology_theory.discrete_topology]
uniform_distribution [file, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_entourage [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_fun [def, in mathcomp.analysis.topology_theory.function_spaces]
uniform_fun_family [def, in mathcomp.analysis.topology_theory.function_spaces]
Uniform_isComplete [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete [mod, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.axioms [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.axioms_ [rec, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.Build [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.cauchy_cvg [proj, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.Exports [mod, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.identity_builder [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.phant_axioms [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.phant_Build [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isConvexTvs [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs [mod, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.identity_builder [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.locally_convex [proj, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isConvexTvs.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isPseudoMetric [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.axioms [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.axioms_ [rec, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.ball [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.Build [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.Exports [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.identity_builder [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.phant_axioms [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.phant_Build [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
uniform_limit_continuous [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_limit_continuous_subspace [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_nbhs [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_nbhsT [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_pdf [def, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_pdf_ge0 [prf, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_pointwise_compact [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_prob [def, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_pseudometric_sup [prf, in mathcomp.analysis.topology_theory.separation_axioms]
uniform_regular [prf, in mathcomp.analysis.topology_theory.separation_axioms]
uniform_regular [prf, in mathcomp.analysis.normedtype_theory.urysohn]
uniform_restrict_cvg [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_separator [def, in mathcomp.analysis.normedtype_theory.urysohn]
uniform_separatorP [prf, in mathcomp.analysis.normedtype_theory.urysohn]
uniform_separatorW [prf, in mathcomp.analysis.normedtype_theory.urysohn]
uniform_set1 [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_structure [file, in mathcomp.analysis.topology_theory.uniform_structure]
uniform_subset_cvg [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_subset_nbhs [prf, in mathcomp.analysis.topology_theory.function_spaces]
UniformElpiOperations [mod, in mathcomp.analysis.topology_theory.uniform_structure]
UniformNmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Algebra_hasAdd_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Algebra_hasZero_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.choice_hasChoice_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.class [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Exports.join_pseudometric_normed_Zmodule_UniformNmodule_between_pseudometric_normed_Zmodule_PreUniformNmodule_and_pseudometric_normed_Zmodule_TopologicalNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.Exports.join_pseudometric_normed_Zmodule_UniformNmodule_between_pseudometric_normed_Zmodule_TopologicalNmodule_and_uniform_structure_Uniform [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.filter_isFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.filter_selfFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.pseudometric_normed_Zmodule_PreTopologicalNmodule_isTopologicalNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.pseudometric_normed_Zmodule_PreUniformNmodule_isUniformNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.sort [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.type [rec, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.identity_builder [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.opp_unif_continuous [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.phant_axioms [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmodule_isUniformZmodule.phant_Build [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformNmoduleElpiOperations [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_hasAdd_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_hasOpp_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Algebra_hasZero_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.choice_hasChoice_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.class [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_Algebra_BaseZmodule_and_pseudometric_normed_Zmodule_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_NbhsZmodule_and_pseudometric_normed_Zmodule_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_PreTopologicalZmodule_and_pseudometric_normed_Zmodule_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_PreUniformNmodule_and_pseudometric_normed_Zmodule_TopologicalZmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_PreUniformZmodule_and_pseudometric_normed_Zmodule_TopologicalNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_PreUniformZmodule_and_pseudometric_normed_Zmodule_TopologicalZmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_PreUniformZmodule_and_pseudometric_normed_Zmodule_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_TopologicalZmodule_and_pseudometric_normed_Zmodule_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_TopologicalZmodule_and_uniform_structure_Uniform [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.Exports.join_pseudometric_normed_Zmodule_UniformZmodule_between_pseudometric_normed_Zmodule_UniformNmodule_and_Algebra_Zmodule [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.filter_isFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.filter_selfFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.pseudometric_normed_Zmodule_PreTopologicalNmodule_isTopologicalNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.pseudometric_normed_Zmodule_PreUniformNmodule_isUniformNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.pseudometric_normed_Zmodule_TopologicalNmodule_isTopologicalZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.pseudometric_normed_Zmodule_UniformNmodule_isUniformZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.sort [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.type [rec, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmodule.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
UniformZmoduleElpiOperations [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
uniq_fset_keys [prf, in mathcomp.experimental_reals.xfinmap]
unit_R [def, in mathcomp.reals_stdlib.Rstruct]
unsquash [def, in mathcomp.classical.classical_sets]
unsquashK [prf, in mathcomp.classical.classical_sets]
unstable [file, in mathcomp.classical.unstable]
upper_bound [def, in mathcomp.classical.wochoice]
ury_base_inv [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_base_refl [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_base_split [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_unif_covA [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_unif_filter [inst, in mathcomp.analysis.normedtype_theory.urysohn]
ury_unif_inv [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_unif_refl [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_unif_split [prf, in mathcomp.analysis.normedtype_theory.urysohn]
ury_unif_split_iter [prf, in mathcomp.analysis.normedtype_theory.urysohn]
urysohn [file, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn [def, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn' [prf, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn_continuous [prf, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn_eq0 [prf, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn_eq1 [prf, in mathcomp.analysis.normedtype_theory.urysohn]
urysohn_ext_itv [prf, in mathcomp.analysis.numfun]
Urysohn_range [prf, in mathcomp.analysis.normedtype_theory.urysohn]
urysohn_separation [prf, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn_sub0 [prf, in mathcomp.analysis.normedtype_theory.urysohn]
Urysohn_sub1 [prf, in mathcomp.analysis.normedtype_theory.urysohn]
urysohnType [def, in mathcomp.analysis.normedtype_theory.urysohn]