'V' (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 | _ | * |
V (Lemmas)
val_bij_subproof [prf, in mathcomp.classical.functions]val_finsetK [prf, in mathcomp.classical.functions]
valL_bijP [prf, in mathcomp.classical.functions]
valL_inj_subproof [prf, in mathcomp.classical.functions]
valL_injP [prf, in mathcomp.classical.functions]
valL_isfun [prf, in mathcomp.classical.functions]
valL_some_inv [prf, in mathcomp.classical.functions]
valL_surj_subproof [prf, in mathcomp.classical.functions]
valL_surjP [prf, in mathcomp.classical.functions]
valLfunK [prf, in mathcomp.classical.functions]
valLfunP [prf, in mathcomp.classical.functions]
valLK [prf, in mathcomp.classical.functions]
valLR_bijP [prf, in mathcomp.classical.functions]
valLR_injP [prf, in mathcomp.classical.functions]
valLR_surjP [prf, in mathcomp.classical.functions]
valLRE [prf, in mathcomp.classical.functions]
valLRfun_inj [prf, in mathcomp.classical.functions]
valLRfunE [prf, in mathcomp.classical.functions]
valLRK [prf, in mathcomp.classical.functions]
valR_inj_subproof [prf, in mathcomp.classical.functions]
valR_surj_subproof [prf, in mathcomp.classical.functions]
valRK [prf, in mathcomp.classical.functions]
valRP [prf, in mathcomp.classical.functions]
variance_cst [prf, in mathcomp.analysis.probability]
variance_fin_num [prf, in mathcomp.analysis.probability]
variance_ge0 [prf, in mathcomp.analysis.probability]
varianceB [prf, in mathcomp.analysis.probability]
varianceB_cst_l [prf, in mathcomp.analysis.probability]
varianceB_cst_r [prf, in mathcomp.analysis.probability]
varianceD [prf, in mathcomp.analysis.probability]
varianceD_cst_l [prf, in mathcomp.analysis.probability]
varianceD_cst_r [prf, in mathcomp.analysis.probability]
varianceE [prf, in mathcomp.analysis.probability]
varianceN [prf, in mathcomp.analysis.probability]
varianceZ [prf, in mathcomp.analysis.probability]
variation_ge0 [prf, in mathcomp.analysis.realfun]
variation_itv_partitionLR [prf, in mathcomp.analysis.realfun]
variation_le [prf, in mathcomp.analysis.realfun]
variation_next [prf, in mathcomp.analysis.realfun]
variation_nil [prf, in mathcomp.analysis.realfun]
variation_opp_rev [prf, in mathcomp.analysis.realfun]
variation_prev [prf, in mathcomp.analysis.realfun]
variation_rev_opp [prf, in mathcomp.analysis.realfun]
variation_subseq [prf, in mathcomp.analysis.realfun]
variation_zip [prf, in mathcomp.analysis.realfun]
variationD [prf, in mathcomp.analysis.realfun]
variationN [prf, in mathcomp.analysis.realfun]
variations_neq0 [prf, in mathcomp.analysis.realfun]
variations_opp [prf, in mathcomp.analysis.realfun]
variations_variation [prf, in mathcomp.analysis.realfun]
variationsN [prf, in mathcomp.analysis.realfun]
variationsxx [prf, in mathcomp.analysis.realfun]
vitali_collection_partition_ub_gt0 [prf, in mathcomp.analysis.normedtype]
vitali_coverS [prf, in mathcomp.analysis.lebesgue_measure]
vitali_lemma_finite [prf, in mathcomp.analysis.normedtype]
vitali_lemma_finite_cover [prf, in mathcomp.analysis.normedtype]
vitali_lemma_infinite [prf, in mathcomp.analysis.normedtype]
vitali_lemma_infinite_cover [prf, in mathcomp.analysis.normedtype]
vitali_theorem [prf, in mathcomp.analysis.lebesgue_measure]
vitali_theorem_corollary [prf, in mathcomp.analysis.lebesgue_measure]