'N' (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

N (Lemmas)

nadde_eq0 [prf, in mathcomp.reals.constructive_ereal]
nat_nbhs_itv [prf, in mathcomp.analysis.topology_theory.nat_topology]
nat_nondecreasing_is_cvg [prf, in mathcomp.analysis.sequences]
nat_nonempty [prf, in mathcomp.classical.classical_sets]
nat_supremums_neq0 [prf, in mathcomp.classical.classical_sets]
nat_typ_subproof [prf, in mathcomp.reals.signed]
natmul_continuous [prf, in mathcomp.analysis.normedtype]
natmul_measurable [prf, in mathcomp.analysis.lebesgue_measure]
natmul_snum_subproof [prf, in mathcomp.reals.signed]
nbh_finW [prf, in mathcomp.experimental_reals.realseq]
nbh_ninfW [prf, in mathcomp.experimental_reals.realseq]
nbh_pinfW [prf, in mathcomp.experimental_reals.realseq]
nbhs0_le [prf, in mathcomp.analysis.normedtype]
nbhs0_lt [prf, in mathcomp.analysis.topology_theory.num_topology]
nbhs0_lt [prf, in mathcomp.analysis.normedtype]
nbhs0_ltW [prf, in mathcomp.analysis.topology_theory.num_topology]
nbhs0N [prf, in mathcomp.analysis.tvs]
nbhs0N_subproof [prf, in mathcomp.analysis.tvs]
nbhs0P [prf, in mathcomp.analysis.normedtype]
nbhs0Z [prf, in mathcomp.analysis.tvs]
nbhs_ball_norm [prf, in mathcomp.analysis.normedtype]
nbhs_ball_normE [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
nbhs_ballE [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
nbhs_ballP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
nbhs_closedballP [prf, in mathcomp.analysis.normedtype]
nbhs_dnbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
nbhs_dnbhs_neq [prf, in mathcomp.analysis.topology_theory.topology_structure]
nbhs_E [prf, in mathcomp.analysis.topology_theory.uniform_structure]
nbhs_EFin [prf, in mathcomp.analysis.normedtype]
nbhs_entourage [prf, in mathcomp.analysis.topology_theory.uniform_structure]
nbhs_entourageE [prf, in mathcomp.analysis.topology_theory.uniform_structure]
nbhs_ereal_ninfty [prf, in mathcomp.analysis.normedtype]
nbhs_ereal_pinfty [prf, in mathcomp.analysis.normedtype]
nbhs_ex [prf, in mathcomp.analysis.normedtype]
nbhs_filter [prf, in mathcomp.analysis.topology_theory.topology_structure]
nbhs_filter_onE [prf, in mathcomp.classical.filter]
nbhs_filterE [prf, in mathcomp.classical.filter]
nbhs_fin_inbound [prf, in mathcomp.analysis.ereal]
nbhs_fin_out_above [prf, in mathcomp.analysis.ereal]
nbhs_fin_out_above_below [prf, in mathcomp.analysis.ereal]
nbhs_fin_out_below [prf, in mathcomp.analysis.ereal]
nbhs_image_EFin [prf, in mathcomp.analysis.normedtype]
nbhs_infty_ge [prf, in mathcomp.analysis.topology_theory.nat_topology]
nbhs_infty_ger [prf, in mathcomp.analysis.topology_theory.nat_topology]
nbhs_infty_gt [prf, in mathcomp.analysis.topology_theory.nat_topology]
nbhs_interior [prf, in mathcomp.analysis.topology_theory.topology_structure]
nbhs_interval [prf, in mathcomp.analysis.ereal]
nbhs_le [prf, in mathcomp.analysis.normedtype]
nbhs_le_nbhs_norm [prf, in mathcomp.analysis.normedtype]
nbhs_left0P [prf, in mathcomp.analysis.normedtype]
nbhs_left_ge [prf, in mathcomp.analysis.normedtype]
nbhs_left_gt [prf, in mathcomp.analysis.normedtype]
nbhs_left_le [prf, in mathcomp.analysis.normedtype]
nbhs_left_lt [prf, in mathcomp.analysis.normedtype]
nbhs_left_ltBl [prf, in mathcomp.analysis.normedtype]
nbhs_left_neq [prf, in mathcomp.analysis.normedtype]
nbhs_lt [prf, in mathcomp.analysis.normedtype]
nbhs_nbhs_norm [prf, in mathcomp.analysis.normedtype]
nbhs_nearE [prf, in mathcomp.classical.filter]
nbhs_ninfty_le [prf, in mathcomp.analysis.normedtype]
nbhs_ninfty_lt [prf, in mathcomp.analysis.normedtype]
nbhs_ninfty_real [prf, in mathcomp.analysis.normedtype]
nbhs_norm0P [prf, in mathcomp.analysis.normedtype]
nbhs_norm_ball [prf, in mathcomp.analysis.normedtype]
nbhs_norm_ball_norm [prf, in mathcomp.analysis.normedtype]
nbhs_norm_le_nbhs [prf, in mathcomp.analysis.normedtype]
nbhs_normE [prf, in mathcomp.analysis.normedtype]
nbhs_normP [prf, in mathcomp.analysis.normedtype]
nbhs_one_point_compactification_weakE [prf, in mathcomp.analysis.normedtype]
nbhs_oo_down_1e [prf, in mathcomp.analysis.ereal]
nbhs_oo_down_e1 [prf, in mathcomp.analysis.ereal]
nbhs_oo_up_1e [prf, in mathcomp.analysis.ereal]
nbhs_oo_up_e1 [prf, in mathcomp.analysis.ereal]
nbhs_open_ereal_gt [prf, in mathcomp.analysis.normedtype]
nbhs_open_ereal_lt [prf, in mathcomp.analysis.normedtype]
nbhs_open_ereal_ninfty [prf, in mathcomp.analysis.normedtype]
nbhs_open_ereal_pinfty [prf, in mathcomp.analysis.normedtype]
nbhs_pinfty_ge [prf, in mathcomp.analysis.normedtype]
nbhs_pinfty_gt [prf, in mathcomp.analysis.normedtype]
nbhs_pinfty_real [prf, in mathcomp.analysis.normedtype]
nbhs_prodX_subspace_inE [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_pt_comp [prf, in mathcomp.analysis_stdlib.Rstruct_topology]
nbhs_right0P [prf, in mathcomp.analysis.normedtype]
nbhs_right_ge [prf, in mathcomp.analysis.normedtype]
nbhs_right_gt [prf, in mathcomp.analysis.normedtype]
nbhs_right_le [prf, in mathcomp.analysis.normedtype]
nbhs_right_lt [prf, in mathcomp.analysis.normedtype]
nbhs_right_ltDr [prf, in mathcomp.analysis.normedtype]
nbhs_right_ltW [prf, in mathcomp.analysis.normedtype]
nbhs_right_neq [prf, in mathcomp.analysis.normedtype]
nbhs_singleton [prf, in mathcomp.analysis.topology_theory.topology_structure]
nbhs_subspace_ex [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_filter [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_in [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_interior [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_nbhs [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_out [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_singleton [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspace_subset [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspaceP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspaceP_subproof [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhs_subspaceT [prf, in mathcomp.analysis.topology_theory.subspace_topology]
nbhsB [prf, in mathcomp.analysis.tvs]
nbhsB_subproof [prf, in mathcomp.analysis.tvs]
nbhsC [prf, in mathcomp.analysis.normedtype]
nbhsC_ball [prf, in mathcomp.analysis.normedtype]
nbhsDl [prf, in mathcomp.analysis.normedtype]
nbhsDr [prf, in mathcomp.analysis.normedtype]
nbhsE [prf, in mathcomp.analysis.topology_theory.topology_structure]
nbhsN [prf, in mathcomp.analysis.normedtype]
nbhsN_subproof [prf, in mathcomp.analysis.tvs]
nbhsNe [prf, in mathcomp.analysis.ereal]
nbhsNimage [prf, in mathcomp.analysis.normedtype]
nbhsNKe [prf, in mathcomp.analysis.ereal]
nbhsP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
nbhsr0P [prf, in mathcomp.analysis.normedtype]
nbhsT [prf, in mathcomp.analysis.tvs]
nbhsT_subproof [prf, in mathcomp.analysis.tvs]
nbhsx_ballx [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
nbhsZ [prf, in mathcomp.analysis.tvs]
nboundedC [prf, in mathcomp.experimental_reals.realseq]
nboundedP [prf, in mathcomp.experimental_reals.realseq]
ncvg_abs [prf, in mathcomp.experimental_reals.realseq]
ncvg_abs0 [prf, in mathcomp.experimental_reals.realseq]
ncvg_eq [prf, in mathcomp.experimental_reals.realseq]
ncvg_eq_from [prf, in mathcomp.experimental_reals.realseq]
ncvg_geC [prf, in mathcomp.experimental_reals.realseq]
ncvg_gt [prf, in mathcomp.experimental_reals.realseq]
ncvg_homo_le [prf, in mathcomp.experimental_reals.realseq]
ncvg_homo_lt [prf, in mathcomp.experimental_reals.realseq]
ncvg_le [prf, in mathcomp.experimental_reals.realseq]
ncvg_le_from [prf, in mathcomp.experimental_reals.realseq]
ncvg_leC [prf, in mathcomp.experimental_reals.realseq]
ncvg_lt [prf, in mathcomp.experimental_reals.realseq]
ncvg_mono [prf, in mathcomp.experimental_reals.realsum]
ncvg_mono_bnd [prf, in mathcomp.experimental_reals.realsum]
ncvg_nbounded [prf, in mathcomp.experimental_reals.realseq]
ncvg_shift [prf, in mathcomp.experimental_reals.realseq]
ncvg_sub [prf, in mathcomp.experimental_reals.realseq]
ncvg_sum [prf, in mathcomp.experimental_reals.realsum]
ncvg_uniq [prf, in mathcomp.experimental_reals.realseq]
ncvgB [prf, in mathcomp.experimental_reals.realseq]
ncvgC [prf, in mathcomp.experimental_reals.realseq]
ncvgD [prf, in mathcomp.experimental_reals.realseq]
ncvgM [prf, in mathcomp.experimental_reals.realseq]
ncvgMl [prf, in mathcomp.experimental_reals.realseq]
ncvgMr [prf, in mathcomp.experimental_reals.realseq]
ncvgN [prf, in mathcomp.experimental_reals.realseq]
ncvgN_fin [prf, in mathcomp.experimental_reals.realseq]
ncvgZ [prf, in mathcomp.experimental_reals.realseq]
nd_approx [prf, in mathcomp.analysis.lebesgue_integral]
nd_ge0_integral_lim [prf, in mathcomp.analysis.lebesgue_integral]
nd_nnsfun_approx [prf, in mathcomp.analysis.lebesgue_integral]
nd_sintegral_lim [prf, in mathcomp.analysis.lebesgue_integral]
nd_sintegral_lim_lemma [prf, in mathcomp.analysis.lebesgue_integral]
ndline_pathE [prf, in mathcomp.classical.set_interval]
near [prf, in mathcomp.classical.filter]
near2_curry [prf, in mathcomp.classical.filter]
near2_pair [prf, in mathcomp.classical.filter]
near_acc [prf, in mathcomp.classical.filter]
near_andP [prf, in mathcomp.classical.filter]
near_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
near_bind [prf, in mathcomp.analysis.topology_theory.topology_structure]
near_can_continuous [prf, in mathcomp.analysis.realfun]
near_can_continuousAcan_sym [prf, in mathcomp.analysis.realfun]
near_continuous_can_sym [prf, in mathcomp.analysis.realfun]
near_covering_withinP [prf, in mathcomp.analysis.topology_theory.compact]
near_cst_continuous [prf, in mathcomp.analysis.topology_theory.topology_structure]
near_davg [prf, in mathcomp.analysis.lebesgue_integral]
near_eq_cvg [prf, in mathcomp.classical.filter]
near_filter_onE [prf, in mathcomp.classical.filter]
near_fun [prf, in mathcomp.classical.filter]
near_in_itvNyo [prf, in mathcomp.analysis.normedtype]
near_in_itvoo [prf, in mathcomp.analysis.normedtype]
near_in_itvoy [prf, in mathcomp.analysis.normedtype]
near_infty_natSinv_expn_lt [prf, in mathcomp.analysis.normedtype]
near_infty_natSinv_lt [prf, in mathcomp.analysis.normedtype]
near_inftyS [prf, in mathcomp.analysis.topology_theory.nat_topology]
near_join [prf, in mathcomp.analysis.topology_theory.topology_structure]
near_key [prf, in mathcomp.classical.filter]
near_map [prf, in mathcomp.classical.filter]
near_map2 [prf, in mathcomp.classical.filter]
near_mapi [prf, in mathcomp.classical.filter]
near_nbhs [prf, in mathcomp.classical.filter]
near_nbhs_norm [prf, in mathcomp.analysis.normedtype]
near_nondecreasing_is_cvgn [prf, in mathcomp.analysis.sequences]
near_nonincreasing_is_cvgn [prf, in mathcomp.analysis.sequences]
near_pair [prf, in mathcomp.classical.filter]
near_pinfty_div2 [prf, in mathcomp.analysis.normedtype]
near_powerset_filter_fromP [prf, in mathcomp.classical.filter]
near_powerset_map [prf, in mathcomp.classical.filter]
near_powerset_map_monoE [prf, in mathcomp.classical.filter]
near_shift [prf, in mathcomp.analysis.normedtype]
near_skip_subproof [prf, in mathcomp.classical.filter]
near_small_set [prf, in mathcomp.classical.filter]
near_swap [prf, in mathcomp.classical.filter]
near_withinE [prf, in mathcomp.classical.filter]
near_withinT [prf, in mathcomp.classical.filter]
nearE [prf, in mathcomp.classical.filter]
neari_eq_loc [prf, in mathcomp.classical.filter]
nearN [prf, in mathcomp.analysis.normedtype]
nearP_dep [prf, in mathcomp.classical.filter]
nearT [prf, in mathcomp.classical.filter]
nearW [prf, in mathcomp.classical.filter]
neg_tv_bounded_variation [prf, in mathcomp.analysis.realfun]
neg_tv_nondecreasing [prf, in mathcomp.analysis.realfun]
neg_tv_right_continuous [prf, in mathcomp.analysis.realfun]
negative_set0 [prf, in mathcomp.analysis.charge]
negative_set_charge_le0 [prf, in mathcomp.analysis.charge]
negative_setU [prf, in mathcomp.analysis.charge]
negligible_bigcup [prf, in mathcomp.analysis.measure]
negligible_bigsetU [prf, in mathcomp.analysis.measure]
negligible_integrable [prf, in mathcomp.analysis.lebesgue_integral]
negligible_integral [prf, in mathcomp.analysis.lebesgue_integral]
negligible_outer_measure [prf, in mathcomp.analysis.lebesgue_measure]
negligible_set0 [prf, in mathcomp.analysis.measure]
negligible_sub_caratheodory [prf, in mathcomp.analysis.lebesgue_measure]
negligibleI [prf, in mathcomp.analysis.measure]
negligibleP [prf, in mathcomp.analysis.measure]
negligibleS [prf, in mathcomp.analysis.measure]
negligibleU [prf, in mathcomp.analysis.measure]
Negz_snum_subproof [prf, in mathcomp.reals.signed]
neitv_bnd1 [prf, in mathcomp.classical.set_interval]
neitv_bnd2 [prf, in mathcomp.classical.set_interval]
neitv_lt_bnd [prf, in mathcomp.classical.set_interval]
neitv_Rhull [prf, in mathcomp.analysis.normedtype]
neitvE [prf, in mathcomp.classical.set_interval]
neitvP [prf, in mathcomp.classical.set_interval]
neq0 [prf, in mathcomp.reals.signed]
neq0_fine_cvgP [prf, in mathcomp.analysis.normedtype]
neq0_mule_def [prf, in mathcomp.reals.constructive_ereal]
neq0_psum [prf, in mathcomp.experimental_reals.realsum]
NGenCInfty.measurable_itv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
NGenCInfty.measurable_itv_bounded [prf, in mathcomp.analysis.lebesgue_measure]
NGenCInfty.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
nice_lebesgue_differentiation [prf, in mathcomp.analysis.lebesgue_integral]
nicely_shrinking_gt0 [prf, in mathcomp.analysis.lebesgue_integral]
nicely_shrinking_lty [prf, in mathcomp.analysis.lebesgue_integral]
ninfty_snum_subproof [prf, in mathcomp.reals.constructive_ereal]
ninftyN [prf, in mathcomp.analysis.normedtype]
nlim_bump [prf, in mathcomp.experimental_reals.realseq]
nlim_lift [prf, in mathcomp.experimental_reals.realseq]
nlim_ncvg [prf, in mathcomp.experimental_reals.realseq]
nlim_out [prf, in mathcomp.experimental_reals.realseq]
nlim_sum [prf, in mathcomp.experimental_reals.realseq]
nlim_sumR [prf, in mathcomp.experimental_reals.realseq]
nlim_sup [prf, in mathcomp.experimental_reals.realseq]
nlimC [prf, in mathcomp.experimental_reals.realseq]
nlimD [prf, in mathcomp.experimental_reals.realseq]
nlimE [prf, in mathcomp.experimental_reals.realseq]
nlimP [prf, in mathcomp.experimental_reals.realseq]
nmule_lge0 [prf, in mathcomp.reals.constructive_ereal]
nmule_lgt0 [prf, in mathcomp.reals.constructive_ereal]
nmule_lle0 [prf, in mathcomp.reals.constructive_ereal]
nmule_llt0 [prf, in mathcomp.reals.constructive_ereal]
nmule_rge0 [prf, in mathcomp.reals.constructive_ereal]
nmule_rgt0 [prf, in mathcomp.reals.constructive_ereal]
nmule_rle0 [prf, in mathcomp.reals.constructive_ereal]
nmule_rlt0 [prf, in mathcomp.reals.constructive_ereal]
nneg_neq0_poweRB_def [prf, in mathcomp.analysis.exp]
nneg_neq0_poweRD_def [prf, in mathcomp.analysis.exp]
nneseries_addn [prf, in mathcomp.analysis.sequences]
nneseries_esum [prf, in mathcomp.analysis.esum]
nneseries_ge0 [prf, in mathcomp.analysis.sequences]
nneseries_interchange [prf, in mathcomp.analysis.esum]
nneseries_lim_ge [prf, in mathcomp.analysis.sequences]
nneseries_pinfty [prf, in mathcomp.analysis.sequences]
nneseries_recl [prf, in mathcomp.analysis.sequences]
nneseries_split [prf, in mathcomp.analysis.sequences]
nneseries_split_cond [prf, in mathcomp.analysis.sequences]
nneseries_sum [prf, in mathcomp.analysis.sequences]
nneseries_sum_bigcup [prf, in mathcomp.analysis.esum]
nneseries_sum_nat [prf, in mathcomp.analysis.sequences]
nneseries_tail_cvg [prf, in mathcomp.analysis.sequences]
nneseriesD [prf, in mathcomp.analysis.sequences]
nneseriesZl [prf, in mathcomp.analysis.sequences]
nnfun_muleindic_ge0 [prf, in mathcomp.analysis.lebesgue_integral]
nngE [prf, in mathcomp.reals.signed]
nnseries_is_cvg [prf, in mathcomp.analysis.sequences]
nnsfun_approxE [prf, in mathcomp.analysis.lebesgue_integral]
nnsfun_cover [prf, in mathcomp.analysis.lebesgue_integral]
nnsfun_coverT [prf, in mathcomp.analysis.lebesgue_integral]
nnsfun_mulemu_ge0 [prf, in mathcomp.analysis.lebesgue_integral]
no_finite_support [prf, in mathcomp.classical.fsbigop]
nondecreasing_at_left_at_right [prf, in mathcomp.analysis.realfun]
nondecreasing_at_left_is_cvgr [prf, in mathcomp.analysis.realfun]
nondecreasing_at_right_cvge [prf, in mathcomp.analysis.realfun]
nondecreasing_at_right_cvgr [prf, in mathcomp.analysis.realfun]
nondecreasing_at_right_is_cvge [prf, in mathcomp.analysis.realfun]
nondecreasing_at_right_is_cvgr [prf, in mathcomp.analysis.realfun]
nondecreasing_bigsetU_seqD [prf, in mathcomp.analysis.sequences]
nondecreasing_bounded_variation [prf, in mathcomp.analysis.realfun]
nondecreasing_cvg_mu [prf, in mathcomp.analysis.measure]
nondecreasing_cvge [prf, in mathcomp.analysis.realfun]
nondecreasing_cvgn [prf, in mathcomp.analysis.sequences]
nondecreasing_cvgn_le [prf, in mathcomp.analysis.sequences]
nondecreasing_cvgr [prf, in mathcomp.analysis.realfun]
nondecreasing_dvgn_lt [prf, in mathcomp.analysis.sequences]
nondecreasing_einfs [prf, in mathcomp.analysis.sequences]
nondecreasing_fun_itv_partition [prf, in mathcomp.analysis.realfun]
nondecreasing_funN [prf, in mathcomp.analysis.realfun]
nondecreasing_infs [prf, in mathcomp.analysis.sequences]
nondecreasing_is_cvge [prf, in mathcomp.analysis.realfun]
nondecreasing_is_cvgn [prf, in mathcomp.analysis.sequences]
nondecreasing_opp [prf, in mathcomp.analysis.sequences]
nondecreasing_right_continuousP [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
nondecreasing_seqD [prf, in mathcomp.analysis.sequences]
nondecreasing_seqP [prf, in mathcomp.analysis.sequences]
nondecreasing_series [prf, in mathcomp.analysis.sequences]
nondecreasing_total_variation [prf, in mathcomp.analysis.realfun]
nondecreasing_variation [prf, in mathcomp.analysis.realfun]
nonempty_image [prf, in mathcomp.classical.classical_sets]
nonempty_preimage [prf, in mathcomp.classical.classical_sets]
nonempty_preimage_setI [prf, in mathcomp.classical.classical_sets]
nonemptyN [prf, in mathcomp.classical.set_interval]
nonincreasing_at_left_at_right [prf, in mathcomp.analysis.realfun]
nonincreasing_at_right_cvge [prf, in mathcomp.analysis.realfun]
nonincreasing_at_right_cvgr [prf, in mathcomp.analysis.realfun]
nonincreasing_at_right_is_cvge [prf, in mathcomp.analysis.realfun]
nonincreasing_at_right_is_cvgr [prf, in mathcomp.analysis.realfun]
nonincreasing_cvg_mu [prf, in mathcomp.analysis.measure]
nonincreasing_cvgn [prf, in mathcomp.analysis.sequences]
nonincreasing_cvgn_ge [prf, in mathcomp.analysis.sequences]
nonincreasing_esups [prf, in mathcomp.analysis.sequences]
nonincreasing_fun_itv_partition [prf, in mathcomp.analysis.realfun]
nonincreasing_funN [prf, in mathcomp.analysis.realfun]
nonincreasing_is_cvgn [prf, in mathcomp.analysis.sequences]
nonincreasing_opp [prf, in mathcomp.analysis.sequences]
nonincreasing_seqP [prf, in mathcomp.analysis.sequences]
nonincreasing_sups [prf, in mathcomp.analysis.sequences]
nonincreasing_variation [prf, in mathcomp.analysis.realfun]
nonnegeP [prf, in mathcomp.reals.constructive_ereal]
nonnegP [prf, in mathcomp.reals.signed]
nonsubset [prf, in mathcomp.classical.classical_sets]
norm_close_eq [prf, in mathcomp.analysis.normedtype]
norm_closeE [prf, in mathcomp.analysis.normedtype]
norm_continuous [prf, in mathcomp.analysis.normedtype]
norm_cos_eq1 [prf, in mathcomp.analysis.trigo]
norm_cvg0 [prf, in mathcomp.analysis.normedtype]
norm_cvg0P [prf, in mathcomp.analysis.normedtype]
norm_cvg_eq [prf, in mathcomp.analysis.normedtype]
norm_cvg_lim [prf, in mathcomp.analysis.normedtype]
norm_cvg_unique [prf, in mathcomp.analysis.normedtype]
norm_cvgi_lim [prf, in mathcomp.analysis.normedtype]
norm_cvgi_unique [prf, in mathcomp.analysis.normedtype]
norm_hausdorff [prf, in mathcomp.analysis.normedtype]
norm_lim_cst [prf, in mathcomp.analysis.normedtype]
norm_lim_id [prf, in mathcomp.analysis.normedtype]
norm_lim_near_cst [prf, in mathcomp.analysis.normedtype]
norm_powR [prf, in mathcomp.analysis.exp]
norm_sin_eq1 [prf, in mathcomp.analysis.trigo]
norm_snum_subproof [prf, in mathcomp.reals.signed]
normal_completely_regular [prf, in mathcomp.analysis.normedtype]
normal_mx_ortho [prf, in mathcomp.analysis.forms]
normal_openP [prf, in mathcomp.analysis.normedtype]
normal_ortho_mx [prf, in mathcomp.analysis.forms]
normal_separatorP [prf, in mathcomp.analysis.normedtype]
normal_uniform_separator [prf, in mathcomp.analysis.normedtype]
normalC [prf, in mathcomp.analysis.forms]
normalE [prf, in mathcomp.analysis.forms]
normalP [prf, in mathcomp.analysis.forms]
normed_cvg [prf, in mathcomp.analysis.sequences]
normed_series_exp_coeff [prf, in mathcomp.analysis.sequences]
normfZV [prf, in mathcomp.analysis.normedtype]
normm_leW [prf, in mathcomp.analysis.normedtype]
normm_littleo [prf, in mathcomp.analysis.derive]
normm_lt_split [prf, in mathcomp.analysis.normedtype]
normr_measurable [prf, in mathcomp.analysis.lebesgue_measure]
normr_nneg [prf, in mathcomp.analysis.exp]
normrZV [prf, in mathcomp.analysis.normedtype]
not_and3P [prf, in mathcomp.classical.boolp]
not_andE [prf, in mathcomp.classical.boolp]
not_andP [prf, in mathcomp.classical.boolp]
not_exists2P [prf, in mathcomp.classical.boolp]
not_existsP [prf, in mathcomp.classical.boolp]
not_False [prf, in mathcomp.classical.boolp]
not_forallP [prf, in mathcomp.classical.boolp]
not_implyE [prf, in mathcomp.classical.boolp]
not_implyP [prf, in mathcomp.classical.boolp]
not_inj [prf, in mathcomp.classical.boolp]
not_near_at_leftP [prf, in mathcomp.analysis.normedtype]
not_near_at_rightP [prf, in mathcomp.analysis.normedtype]
not_near_inftyP [prf, in mathcomp.analysis.normedtype]
not_near_ninftyP [prf, in mathcomp.analysis.normedtype]
not_orE [prf, in mathcomp.classical.boolp]
not_orP [prf, in mathcomp.classical.boolp]
not_setD1 [prf, in mathcomp.classical.classical_sets]
not_True [prf, in mathcomp.classical.boolp]
notB [prf, in mathcomp.classical.boolp]
notE [prf, in mathcomp.classical.boolp]
notFE [prf, in mathcomp.classical.boolp]
notin_itv_partition [prf, in mathcomp.analysis.realfun]
notin_range_measure [prf, in mathcomp.analysis.probability]
notin_setE [prf, in mathcomp.classical.classical_sets]
notin_setI_preimage [prf, in mathcomp.classical.classical_sets]
notin_xsectionX [prf, in mathcomp.classical.classical_sets]
notin_ysectionX [prf, in mathcomp.classical.classical_sets]
notK [prf, in mathcomp.classical.boolp]
notLR [prf, in mathcomp.classical.boolp]
notP [prf, in mathcomp.classical.boolp]
notRL [prf, in mathcomp.classical.boolp]
notT [prf, in mathcomp.classical.boolp]
notTE [prf, in mathcomp.classical.boolp]
npeseries_le0 [prf, in mathcomp.analysis.sequences]
Nsatz_realType_Setoid_Theory [prf, in mathcomp.reals.nsatz_realtype]
null_set_integral [prf, in mathcomp.analysis.lebesgue_integral]
null_set_setU [prf, in mathcomp.analysis.measure]
num_abs_eq0 [prf, in mathcomp.reals.signed]
num_abs_le [prf, in mathcomp.reals.signed]
num_abs_lt [prf, in mathcomp.reals.signed]
num_abse_eq0 [prf, in mathcomp.reals.constructive_ereal]
num_abse_le [prf, in mathcomp.reals.constructive_ereal]
num_abse_lt [prf, in mathcomp.reals.constructive_ereal]
num_eq [prf, in mathcomp.reals.signed]
num_eq0 [prf, in mathcomp.reals.signed]
num_ge_max [prf, in mathcomp.reals.signed]
num_ge_min [prf, in mathcomp.reals.signed]
num_gee_max [prf, in mathcomp.reals.constructive_ereal]
num_gee_min [prf, in mathcomp.reals.constructive_ereal]
num_gt_max [prf, in mathcomp.reals.signed]
num_gt_min [prf, in mathcomp.reals.signed]
num_gte_max [prf, in mathcomp.reals.constructive_ereal]
num_gte_min [prf, in mathcomp.reals.constructive_ereal]
num_le [prf, in mathcomp.reals.signed]
num_le_max [prf, in mathcomp.reals.signed]
num_le_min [prf, in mathcomp.reals.signed]
num_lee_max [prf, in mathcomp.reals.constructive_ereal]
num_lee_min [prf, in mathcomp.reals.constructive_ereal]
num_lt [prf, in mathcomp.reals.signed]
num_lt_max [prf, in mathcomp.reals.signed]
num_lt_min [prf, in mathcomp.reals.signed]
num_lte_max [prf, in mathcomp.reals.constructive_ereal]
num_lte_min [prf, in mathcomp.reals.constructive_ereal]
num_max [prf, in mathcomp.reals.signed]
num_min [prf, in mathcomp.reals.signed]