Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 22:45 86d65f8d

View on Github →

chore(topology/instances/ennreal): prove nnreal.not_summable_iff_tendsto_nat_at_top (#4670)

  • use ℝ≥0 notation in data/real/ennreal;

  • add ennreal.forall_ne_top, ennreal.exists_ne_top, ennreal.ne_top_equiv_nnreal, ennreal.cinfi_ne_top, ennreal.infi_ne_top, ennreal.csupr_ne_top, ennreal.sup_ne_top, ennreal.supr_ennreal;

  • add nnreal.injective_coe, add @[simp, norm_cast] to nnreal.tendsto_coe, and add nnreal.tendsto_coe_at_top; move nnreal.infi_real_pos_eq_infi_nnreal_pos from ennreal to nnreal;

  • use function.injective instead of an unfolded definition in filter.comap_map;

  • add ennreal.nhds_top', ennreal.tendsto_nhds_top_iff_nnreal, ennreal.tendsto_nhds_top_iff_nat;

  • upgrade ennreal.tendsto_coe_nnreal_nhds_top to an iff, rename to ennreal.tendsto_coe_nhds_top;

  • nnreal.has_sum_iff_tendsto_nat now takes r as an implicit argument;

  • add nnreal.not_summable_iff_tendsto_nat_at_top and not_summable_iff_tendsto_nat_at_top_of_nonneg.

Estimated changes

added theorem ennreal.cinfi_ne_top
modified theorem ennreal.coe_Inf
modified theorem ennreal.coe_Sup
modified theorem ennreal.coe_finset_prod
modified theorem ennreal.coe_finset_sum
modified theorem ennreal.coe_indicator
modified theorem ennreal.coe_inv_two
modified theorem ennreal.coe_le_iff
modified theorem ennreal.coe_max
modified theorem ennreal.coe_min
modified theorem ennreal.coe_mono
modified theorem ennreal.coe_nat
modified theorem ennreal.coe_nnreal_eq
modified theorem ennreal.coe_one
modified theorem ennreal.coe_to_real
modified theorem ennreal.coe_two
modified theorem ennreal.coe_zero
added theorem ennreal.csupr_ne_top
added theorem ennreal.exists_ne_top
modified theorem ennreal.forall_ennreal
added theorem ennreal.forall_ne_top
added theorem ennreal.infi_ne_top
modified theorem ennreal.le_coe_iff
modified theorem ennreal.lt_iff_exists_coe
modified def ennreal.of_nnreal_hom
modified theorem ennreal.some_eq_coe
added theorem ennreal.supr_ennreal
added theorem ennreal.supr_ne_top
modified def ennreal
modified theorem filter.comap_map
added theorem tendsto_nhds_bot_mono'
added theorem tendsto_nhds_bot_mono
added theorem tendsto_nhds_top_mono'
added theorem tendsto_nhds_top_mono
added theorem ennreal.nhds_top'
modified theorem ennreal.nhds_top
added theorem nnreal.map_coe_at_top
added theorem nnreal.tendsto_coe'
modified theorem nnreal.tendsto_coe