U (Global Index)
| 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 |
U
u_cons [abbrev, in mathcomp.algebra.tensor]u_cons [abbrev, in mathcomp.algebra.tensor]
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]
ubn_eq_spec [ind, in mathcomp.boot.ssrnat]
ubn_geq_spec [ind, in mathcomp.boot.ssrnat]
ubn_leq_spec [ind, in mathcomp.boot.ssrnat]
UbnEq [constr, in mathcomp.boot.ssrnat]
UbnGeq [constr, in mathcomp.boot.ssrnat]
UbnLeq [constr, in mathcomp.boot.ssrnat]
ubnP [prf, in mathcomp.boot.ssrnat]
ubnPeq [prf, in mathcomp.boot.ssrnat]
ubnPgeq [prf, in mathcomp.boot.ssrnat]
ubnPleq [prf, in mathcomp.boot.ssrnat]
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]
ucn0 [prf, in mathcomp.solvable.nilpotent]
ucn1 [prf, in mathcomp.solvable.nilpotent]
ucn_bigcprod [prf, in mathcomp.solvable.nilpotent]
ucn_bigdprod [prf, in mathcomp.solvable.nilpotent]
ucn_central [prf, in mathcomp.solvable.nilpotent]
ucn_char [prf, in mathcomp.solvable.nilpotent]
ucn_comm [prf, in mathcomp.solvable.nilpotent]
ucn_cprod [prf, in mathcomp.solvable.nilpotent]
ucn_dprod [prf, in mathcomp.solvable.nilpotent]
ucn_gFun [def, in mathcomp.solvable.nilpotent]
ucn_group_set [prf, in mathcomp.solvable.nilpotent]
ucn_id [prf, in mathcomp.solvable.nilpotent]
ucn_igFun [def, in mathcomp.solvable.nilpotent]
ucn_lcnP [prf, in mathcomp.solvable.nilpotent]
ucn_nil_classP [prf, in mathcomp.solvable.nilpotent]
ucn_nilpotent [prf, in mathcomp.solvable.nilpotent]
ucn_norm [prf, in mathcomp.solvable.nilpotent]
ucn_normal [prf, in mathcomp.solvable.nilpotent]
ucn_normalS [prf, in mathcomp.solvable.nilpotent]
ucn_pgFun [def, in mathcomp.solvable.nilpotent]
ucn_pmap [prf, in mathcomp.solvable.nilpotent]
ucn_sub [prf, in mathcomp.solvable.nilpotent]
ucn_sub_geq [prf, in mathcomp.solvable.nilpotent]
ucn_subS [prf, in mathcomp.solvable.nilpotent]
ucnE [prf, in mathcomp.solvable.nilpotent]
ucnP [prf, in mathcomp.solvable.nilpotent]
ucnSn [prf, in mathcomp.solvable.nilpotent]
ucnSnR [prf, in mathcomp.solvable.nilpotent]
ucycle [def, in mathcomp.boot.path]
ucycle_cycle [prf, in mathcomp.boot.path]
ucycle_uniq [prf, in mathcomp.boot.path]
ucycleb [def, in mathcomp.boot.path]
ufcycle [abbrev, in mathcomp.boot.path]
ulsubmx [def, in mathcomp.algebra.matrix]
ulsubmx_diag [prf, in mathcomp.algebra.matrix]
ulsubmx_trig [prf, in mathcomp.algebra.matrix]
ulsubmxEsub [prf, in mathcomp.algebra.matrix]
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]
UMagma [abbrev, in mathcomp.boot.monoid]
UMagma [mod, in mathcomp.boot.monoid]
UMagma.axioms_ [rec, in mathcomp.boot.monoid]
UMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
UMagma.class [proj, in mathcomp.boot.monoid]
UMagma.clone [abbrev, in mathcomp.boot.monoid]
UMagma.copy [abbrev, in mathcomp.boot.monoid]
UMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
UMagma.Exports [mod, in mathcomp.boot.monoid]
UMagma.Exports.umagmaType [abbrev, in mathcomp.boot.monoid]
UMagma.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
UMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
UMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
UMagma.on [abbrev, in mathcomp.boot.monoid]
UMagma.on_ [abbrev, in mathcomp.boot.monoid]
UMagma.pack_ [def, in mathcomp.boot.monoid]
UMagma.phant_clone [def, in mathcomp.boot.monoid]
UMagma.phant_on_ [def, in mathcomp.boot.monoid]
UMagma.sort [proj, in mathcomp.boot.monoid]
UMagma.type [rec, in mathcomp.boot.monoid]
umagma_closed [def, in mathcomp.boot.monoid]
UMagma_isMonoid [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid [mod, in mathcomp.boot.monoid]
UMagma_isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid.axioms_ [rec, in mathcomp.boot.monoid]
UMagma_isMonoid.Build [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid.Exports [mod, in mathcomp.boot.monoid]
UMagma_isMonoid.mulgA [proj, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_Build [def, in mathcomp.boot.monoid]
UMagmaClosed [abbrev, in mathcomp.boot.monoid]
UMagmaClosed [mod, in mathcomp.boot.monoid]
UMagmaClosed.axioms_ [rec, in mathcomp.boot.monoid]
UMagmaClosed.class [proj, in mathcomp.boot.monoid]
UMagmaClosed.clone [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.copy [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.Exports [mod, in mathcomp.boot.monoid]
UMagmaClosed.Exports.umagmaClosed [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.monoid_isMul1Closed_mixin [proj, in mathcomp.boot.monoid]
UMagmaClosed.monoid_isMulClosed_mixin [proj, in mathcomp.boot.monoid]
UMagmaClosed.on [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.on_ [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.pack_ [def, in mathcomp.boot.monoid]
UMagmaClosed.phant_clone [def, in mathcomp.boot.monoid]
UMagmaClosed.phant_on_ [def, in mathcomp.boot.monoid]
UMagmaClosed.sort [proj, in mathcomp.boot.monoid]
UMagmaClosed.type [rec, in mathcomp.boot.monoid]
UMagmaClosedElpiOperations [mod, in mathcomp.boot.monoid]
UMagmaElpiOperations [mod, in mathcomp.boot.monoid]
UMagmaMorphism [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism [mod, in mathcomp.boot.monoid]
UMagmaMorphism.axioms_ [rec, in mathcomp.boot.monoid]
UMagmaMorphism.class [proj, in mathcomp.boot.monoid]
UMagmaMorphism.clone [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.copy [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.Exports [mod, in mathcomp.boot.monoid]
UMagmaMorphism.monoid_isMultiplicative_mixin [proj, in mathcomp.boot.monoid]
UMagmaMorphism.monoid_Multiplicative_isUMagmaMorphism_mixin [proj, in mathcomp.boot.monoid]
UMagmaMorphism.on [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.on_ [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.pack_ [def, in mathcomp.boot.monoid]
UMagmaMorphism.phant_clone [def, in mathcomp.boot.monoid]
UMagmaMorphism.phant_on_ [def, in mathcomp.boot.monoid]
UMagmaMorphism.sort [proj, in mathcomp.boot.monoid]
UMagmaMorphism.type [rec, in mathcomp.boot.monoid]
UMagmaMorphismElpiOperations [mod, in mathcomp.boot.monoid]
unbind [def, in mathcomp.classical.functions]
unbump [def, in mathcomp.boot.fintype]
unbumpDl [prf, in mathcomp.boot.fintype]
unbumpK [prf, in mathcomp.boot.fintype]
unbumpKcond [prf, in mathcomp.boot.fintype]
unbumpS [prf, in mathcomp.boot.fintype]
uncurry_continuous [prf, in mathcomp.analysis.topology_theory.function_spaces]
uncurryK [prf, in mathcomp.classical.boolp]
undup [def, in mathcomp.boot.seq]
undup_cat [prf, in mathcomp.boot.seq]
undup_cycle_cons [prf, in mathcomp.boot.fingraph]
undup_flatten_nseq [prf, in mathcomp.boot.seq]
undup_id [prf, in mathcomp.boot.seq]
undup_map_inj [prf, in mathcomp.boot.seq]
undup_nil [prf, in mathcomp.boot.seq]
undup_path [prf, in mathcomp.boot.path]
undup_rcons [prf, in mathcomp.boot.seq]
undup_sorted [prf, in mathcomp.boot.path]
undup_subseq [prf, in mathcomp.boot.seq]
undup_uniq [prf, in mathcomp.boot.seq]
unif_continuous [def, 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_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_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_isTvs [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs [mod, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.identity_builder [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.locally_convex [proj, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
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]
UniformLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_hasAdd_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_hasOpp_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Algebra_hasZero_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.choice_hasChoice_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.class [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_Lmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_Lmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_LSemiModule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_LSemiModule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_NbhsLmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_NbhsLmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreTopologicalLmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreTopologicalLmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreUniformLmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreUniformLmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.filter_isFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.filter_selfFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.GRing_Nmodule_isLSemiModule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.sort [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.tvs_PreUniformLmodule_isUniformLmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.tvs_PreUniformNmodule_isUniformNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.tvs_UniformNmodule_isUniformZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.type [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmoduleElpiOperations [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.Algebra_hasAdd_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.Algebra_hasZero_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.choice_hasChoice_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.class [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.filter_isFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.filter_selfFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.sort [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.tvs_PreUniformNmodule_isUniformNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.type [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.scale_unif_continuous [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.identity_builder [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.opp_unif_continuous [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmoduleElpiOperations [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_hasAdd_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_hasOpp_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Algebra_hasZero_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.axioms_ [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.choice_hasChoice_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.class [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports [mod, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_Algebra_BaseZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_pseudometric_normed_Zmodule_NbhsZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_pseudometric_normed_Zmodule_PreTopologicalZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_pseudometric_normed_Zmodule_PreUniformZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_tvs_UniformNmodule_and_Algebra_Zmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.filter_isFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.filter_selfFiltered_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.sort [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.tvs_PreUniformNmodule_isUniformNmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.tvs_UniformNmodule_isUniformZmodule_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.type [rec, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmoduleElpiOperations [mod, in mathcomp.analysis.normedtype_theory.tvs]
Unify [proj, in mathcomp.reals.signed]
Unify [constr, in mathcomp.reals.signed]
unify [rec, in mathcomp.reals.signed]
unify [ind, in mathcomp.reals.signed]
Unify [proj, in mathcomp.algebra.interval_inference]
Unify [constr, in mathcomp.algebra.interval_inference]
unify [rec, in mathcomp.algebra.interval_inference]
unify [ind, in mathcomp.algebra.interval_inference]
Unify' [proj, in mathcomp.reals.signed]
Unify' [constr, in mathcomp.reals.signed]
unify' [rec, in mathcomp.reals.signed]
unify' [ind, in mathcomp.reals.signed]
Unify' [proj, in mathcomp.algebra.interval_inference]
Unify' [constr, in mathcomp.algebra.interval_inference]
unify' [rec, in mathcomp.algebra.interval_inference]
unify' [ind, in mathcomp.algebra.interval_inference]
unify'P [inst, in mathcomp.reals.signed]
unify'P [inst, in mathcomp.algebra.interval_inference]
unify_itv [abbrev, in mathcomp.algebra.interval_inference]
unify_nz [abbrev, in mathcomp.reals.signed]
unify_r [abbrev, in mathcomp.reals.signed]
uniq [def, in mathcomp.boot.seq]
uniq4_uniq6 [prf, in mathcomp.solvable.burnside_app]
uniq_cat_inLR [prf, in mathcomp.boot.seq]
uniq_cat_inRL [prf, in mathcomp.boot.seq]
uniq_catC [prf, in mathcomp.boot.seq]
uniq_catCA [prf, in mathcomp.boot.seq]
uniq_eqseq_pivotl [prf, in mathcomp.boot.seq]
uniq_eqseq_pivotr [prf, in mathcomp.boot.seq]
uniq_leq_size [prf, in mathcomp.boot.seq]
uniq_map_inj_in [prf, in mathcomp.boot.seq]
uniq_min_size [prf, in mathcomp.boot.seq]
uniq_normal_Hall [prf, in mathcomp.solvable.pgroup]
uniq_pairwise [prf, in mathcomp.boot.seq]
uniq_perm [prf, in mathcomp.boot.seq]
uniq_roots [def, in mathcomp.algebra.poly]
uniq_roots_prod_XsubC [prf, in mathcomp.algebra.poly]
uniq_rootsE [prf, in mathcomp.algebra.poly]
uniq_size_uniq [prf, in mathcomp.boot.seq]
uniq_sub_le_big [prf, in mathcomp.boot.bigop]
uniq_sub_le_big_cond [prf, in mathcomp.boot.bigop]
uniq_subseq_pivot [prf, in mathcomp.boot.seq]
uniq_traject_porbit [prf, in mathcomp.finite_group.perm]
uniqP [prf, in mathcomp.boot.seq]
uniqPn [prf, in mathcomp.boot.seq]
unit_enumP [prf, in mathcomp.boot.fintype]
unit_eqP [prf, in mathcomp.boot.eqtype]
unit_Zp_expg [prf, in mathcomp.algebra.zmodp]
unit_Zp_mulgC [prf, in mathcomp.algebra.zmodp]
UnitAlgebra_isFalgebra [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra [mod, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.axioms [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.axioms_ [rec, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.Build [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.Exports [mod, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.phant_axioms [def, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.phant_Build [def, in mathcomp.field.falgebra]
unitarymx [def, in mathcomp.algebra.spectral]
unitarymx_key [prf, in mathcomp.algebra.spectral]
unitarymx_keyed [def, in mathcomp.algebra.spectral]
unitarymx_unit [prf, in mathcomp.algebra.spectral]
unitarymxP [prf, in mathcomp.algebra.spectral]
unitFpE [prf, in mathcomp.algebra.zmodp]
unitmx [def, in mathcomp.algebra.matrix]
unitmx1 [prf, in mathcomp.algebra.matrix]
unitmx_inv [prf, in mathcomp.algebra.matrix]
unitmx_mul [prf, in mathcomp.algebra.matrix]
unitmx_perm [prf, in mathcomp.algebra.matrix]
unitmx_tr [prf, in mathcomp.algebra.matrix]
unitmxE [prf, in mathcomp.algebra.matrix]
unitmxZ [prf, in mathcomp.algebra.matrix]
unitr_algid1 [prf, in mathcomp.field.falgebra]
unitr_n0expz [prf, in mathcomp.algebra.ssrint]
unitr_trmx [prf, in mathcomp.algebra.matrix]
UnitRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient [mod, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasAdd_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasOpp_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasZero_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.axioms_ [rec, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.choice_hasChoice_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.class [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.clone [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.copy [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.eqtype_hasDecEq_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports [mod, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_generic_quotient_EqQuotient_and_GRing_UnitRing [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_generic_quotient_Quotient_and_GRing_UnitRing [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_GRing_UnitRing_and_ring_quotient_ZmodQuotient [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_ring_quotient_NzRingQuotient_and_GRing_UnitRing [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.unitRingQuotType [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.generic_quotient_isEqQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.generic_quotient_isQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_Nmodule_isPzSemiRing_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_NzRing_hasMulInverse_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_PzSemiRing_isNonZero_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.on [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.on_ [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.pack_ [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.phant_clone [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.phant_on_ [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isNzRingQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isUnitRingQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isZmodQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.sort [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.type [rec, in mathcomp.algebra.ring_quotient]
UnitRingQuotientElpiOperations [mod, in mathcomp.algebra.ring_quotient]
unitrXz [prf, in mathcomp.algebra.ssrint]
units_Zp [def, in mathcomp.algebra.zmodp]
units_Zp_abelian [prf, in mathcomp.algebra.zmodp]
units_Zp_cyclic [prf, in mathcomp.solvable.cyclic]
units_Zp_group [def, in mathcomp.algebra.zmodp]
unitt [def, in mathcomp.algebra.tensor]
unity_rootE [prf, in mathcomp.algebra.poly]
unity_rootP [prf, in mathcomp.algebra.poly]
UnityRootTheory [mod, in mathcomp.algebra.poly]
UnityRootTheory.eq_prim_root_expr [def, in mathcomp.algebra.poly]
UnityRootTheory.fmorph_primitive_root [def, in mathcomp.algebra.poly]
UnityRootTheory.fmorph_unity_root [def, in mathcomp.algebra.poly]
UnityRootTheory.max_unity_roots [def, in mathcomp.algebra.poly]
UnityRootTheory.mem_unity_roots [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_expr_mod [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_expr_order [abbrev, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_dvd [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_exists [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_gt0 [abbrev, in mathcomp.algebra.poly]
UnityRootTheory.prim_rootP [def, in mathcomp.algebra.poly]
UnityRootTheory.rmorph_unity_root [def, in mathcomp.algebra.poly]
UnityRootTheory.unity_rootE [def, in mathcomp.algebra.poly]
UnityRootTheory.unity_rootP [def, in mathcomp.algebra.poly]
unitZpE [prf, in mathcomp.algebra.zmodp]
unlift [def, in mathcomp.boot.fintype]
unlift_none [prf, in mathcomp.boot.fintype]
unlift_some [prf, in mathcomp.boot.fintype]
unlift_spec [ind, in mathcomp.boot.fintype]
UnliftNone [constr, in mathcomp.boot.fintype]
unliftP [prf, in mathcomp.boot.fintype]
UnliftSome [constr, in mathcomp.boot.fintype]
unlockable_enum_rank_in [def, in mathcomp.boot.fintype]
unpickle [def, in mathcomp.finmap.finmap]
unpickle [def, in mathcomp.boot.choice]
unpickle_seq [def, in mathcomp.boot.choice]
unpickle_tagged [def, in mathcomp.boot.choice]
unpickleK [prf, in mathcomp.finmap.finmap]
unset1 [def, in mathcomp.boot.finset]
unset10 [prf, in mathcomp.boot.finset]
unset1K [prf, in mathcomp.boot.finset]
unset1N1 [prf, in mathcomp.boot.finset]
unsplit [def, in mathcomp.boot.fintype]
unsplitK [prf, in mathcomp.boot.fintype]
unsquash [def, in mathcomp.classical.classical_sets]
unsquashK [prf, in mathcomp.classical.classical_sets]
unstable [file, in mathcomp.classical.unstable]
untag [def, in mathcomp.boot.eqtype]
untag_cst [prf, in mathcomp.boot.eqtype]
untag_dflt [prf, in mathcomp.boot.eqtype]
untag_with [def, in mathcomp.boot.eqtype]
untag_with_bij [prf, in mathcomp.boot.eqtype]
untag_withK [prf, in mathcomp.boot.eqtype]
untagE [prf, in mathcomp.boot.eqtype]
unzip1 [def, in mathcomp.boot.seq]
unzip1_map_nth_zip [prf, in mathcomp.boot.seq]
unzip1_zip [prf, in mathcomp.boot.seq]
unzip2 [def, in mathcomp.boot.seq]
unzip2_map_nth_zip [prf, in mathcomp.boot.seq]
unzip2_zip [prf, in mathcomp.boot.seq]
up_expnK [prf, in mathcomp.boot.prime]
up_log [def, in mathcomp.boot.prime]
up_log0 [prf, in mathcomp.boot.prime]
up_log1 [prf, in mathcomp.boot.prime]
up_log2_double [prf, in mathcomp.boot.prime]
up_log2S [prf, in mathcomp.boot.prime]
up_log_bounds [prf, in mathcomp.boot.prime]
up_log_eq [prf, in mathcomp.boot.prime]
up_log_eq0 [prf, in mathcomp.boot.prime]
up_log_gt0 [prf, in mathcomp.boot.prime]
up_log_gtn [prf, in mathcomp.boot.prime]
up_log_min [prf, in mathcomp.boot.prime]
up_log_trunc_log [prf, in mathcomp.boot.prime]
up_logMp [prf, in mathcomp.boot.prime]
up_lognn [prf, in mathcomp.boot.prime]
up_logP [prf, in mathcomp.boot.prime]
uphalf [def, in mathcomp.boot.ssrnat]
uphalf_double [prf, in mathcomp.boot.ssrnat]
uphalf_gt0 [prf, in mathcomp.boot.ssrnat]
uphalf_half [prf, in mathcomp.boot.ssrnat]
uphalf_leq [prf, in mathcomp.boot.ssrnat]
uphalfE [prf, in mathcomp.boot.ssrnat]
uphalfK [prf, in mathcomp.boot.ssrnat]
upper_bound [def, in mathcomp.classical.wochoice]
upper_central_at [def, in mathcomp.solvable.nilpotent]
upper_central_at_group [def, in mathcomp.solvable.nilpotent]
ursubmx [def, in mathcomp.algebra.matrix]
ursubmx_trig [prf, in mathcomp.algebra.matrix]
ursubmxEsub [prf, in mathcomp.algebra.matrix]
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]
usubmx [def, in mathcomp.algebra.matrix]
usubmx_key [prf, in mathcomp.algebra.matrix]
usubmxEsub [prf, in mathcomp.algebra.matrix]