U (Lemmas)
| 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 (Lemmas)
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]
ubnP [prf, in mathcomp.boot.ssrnat]
ubnPeq [prf, in mathcomp.boot.ssrnat]
ubnPgeq [prf, in mathcomp.boot.ssrnat]
ubnPleq [prf, in mathcomp.boot.ssrnat]
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_group_set [prf, in mathcomp.solvable.nilpotent]
ucn_id [prf, 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_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_cycle [prf, in mathcomp.boot.path]
ucycle_uniq [prf, in mathcomp.boot.path]
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]
ultraFilterLemma [prf, in mathcomp.classical.filter]
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_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_continuousP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
uniform_completely_regular [prf, in mathcomp.analysis.normedtype_theory.urysohn]
uniform_entourage [prf, in mathcomp.analysis.topology_theory.function_spaces]
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_ge0 [prf, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_pointwise_compact [prf, in mathcomp.analysis.topology_theory.function_spaces]
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_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_subset_cvg [prf, in mathcomp.analysis.topology_theory.function_spaces]
uniform_subset_nbhs [prf, in mathcomp.analysis.topology_theory.function_spaces]
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_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]
unitarymx_key [prf, in mathcomp.algebra.spectral]
unitarymx_unit [prf, in mathcomp.algebra.spectral]
unitarymxP [prf, in mathcomp.algebra.spectral]
unitFpE [prf, in mathcomp.algebra.zmodp]
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]
unitrXz [prf, in mathcomp.algebra.ssrint]
units_Zp_abelian [prf, in mathcomp.algebra.zmodp]
units_Zp_cyclic [prf, in mathcomp.solvable.cyclic]
unity_rootE [prf, in mathcomp.algebra.poly]
unity_rootP [prf, in mathcomp.algebra.poly]
unitZpE [prf, in mathcomp.algebra.zmodp]
unlift_none [prf, in mathcomp.boot.fintype]
unlift_some [prf, in mathcomp.boot.fintype]
unliftP [prf, in mathcomp.boot.fintype]
unpickleK [prf, in mathcomp.finmap.finmap]
unset10 [prf, in mathcomp.boot.finset]
unset1K [prf, in mathcomp.boot.finset]
unset1N1 [prf, in mathcomp.boot.finset]
unsplitK [prf, in mathcomp.boot.fintype]
unsquashK [prf, in mathcomp.classical.classical_sets]
untag_cst [prf, in mathcomp.boot.eqtype]
untag_dflt [prf, 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_map_nth_zip [prf, in mathcomp.boot.seq]
unzip1_zip [prf, 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_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_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]
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_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' [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]
usubmx_key [prf, in mathcomp.algebra.matrix]
usubmxEsub [prf, in mathcomp.algebra.matrix]