Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-28 11:49 cafd1937

View on Github →

chore(*): use filter.eventually (#1897)

  • chore(*): use filter.eventually
  • Update src/measure_theory/integration.lean Co-Authored-By: Yury G. Kudryashov urkud@ya.ru
  • Fix closeds.complete_space.
  • Fix tendsto_integral_of_dominated_convergence
  • Fix tendsto_exp_at_top
  • Fix exists_norm_eq_infi_of_complete_convex
  • Use obtain.
  • Use filter.eventually_of_forall

Estimated changes

modified theorem deriv_congr_of_mem_nhds
modified theorem fderiv_congr_of_mem_nhds
modified theorem mfderiv_congr_of_mem_nhds
modified def measure_theory.all_ae
added theorem filter.eventually_Sup
added theorem filter.eventually_bot
added theorem filter.eventually_sup
added theorem filter.eventually_supr
added theorem filter.eventually_top
added theorem filter.frequently_Sup
added theorem filter.frequently_bot
added theorem filter.frequently_sup
added theorem filter.frequently_supr
added theorem filter.frequently_top
added theorem filter.not_eventually
added theorem filter.not_frequently
modified theorem filter.tendsto_principal
modified def is_max_filter
modified def is_min_filter
modified def filter.Liminf
modified theorem filter.Liminf_eq_supr_Inf
modified def filter.Limsup
modified theorem filter.Limsup_eq_infi_Sup
modified def filter.is_bounded
modified theorem filter.is_cobounded.mk
modified def filter.is_cobounded
modified theorem filter.liminf_eq
modified theorem filter.liminf_eq_supr_infi
modified theorem filter.limsup_eq
modified theorem filter.limsup_eq_infi_supr
modified theorem ge_mem_nhds
modified theorem gt_mem_nhds
modified theorem le_mem_nhds
modified theorem lt_mem_nhds