Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-19 21:18 1bb3d198

View on Github →

refactor(order/filter/basic): add class filter.ne_bot (#3454) This way Lean will f≠ ⊥ in a few most common cases (incl. nhds_ne_bot, at_top_ne_bot) automatically. Other API changes:

  • many lemmas now take [ne_bot l] instead of (hl : l ≠ ⊥);
  • some lemmas got ' versions that take an explicit (hl : ne_bot l);
  • rename ultrafilter_unique to is_ultrafilter.unique;
  • cauchy_downwards is now cauchy.mono (instance arg) and cauchy.mono' (explicit arg);
  • cauchy_map is now cauchy.map;
  • cauchy_comap is now cauchy.comap;
  • totally_bounded_closure is now totally_bounded.closure;
  • totally_bounded_image is now totally_bounded.image;

Estimated changes

modified theorem hyperreal.coe_le_coe
modified theorem filter.at_top_ne_bot
modified theorem filter.comap_ne_bot
modified theorem filter.comap_ne_bot_iff
modified theorem filter.eventually.exists
modified theorem filter.eventually_const
modified theorem filter.frequently_const
modified theorem filter.frequently_of_forall
deleted theorem filter.map_ne_bot
modified theorem filter.map_ne_bot_iff
added theorem filter.ne_bot.map
added theorem filter.ne_bot.mono
added theorem filter.ne_bot.ne
added theorem filter.ne_bot.prod
added def filter.ne_bot
added theorem filter.ne_bot_of_le
modified theorem filter.nonempty_of_mem_sets
modified theorem filter.nonempty_of_ne_bot
modified theorem filter.principal_ne_bot_iff
modified theorem filter.prod_ne_bot
deleted theorem filter.pure_ne_bot
modified theorem filter.tendsto.ne_bot
deleted theorem filter.cofinite_ne_bot
modified theorem filter.const_eventually_eq'
modified theorem filter.const_eventually_eq
modified theorem filter.germ.const_inj
modified theorem filter.germ.const_le_iff
modified theorem filter.lift'_ne_bot_iff
modified theorem filter.lift_ne_bot_iff
deleted theorem filter.mul_ne_bot
added theorem filter.ne_bot.mul
modified theorem filter.exists_ultrafilter
modified theorem filter.hyperfilter_ne_bot
modified def filter.is_ultrafilter
modified theorem filter.le_of_ultrafilter
modified theorem filter.ultrafilter_of_spec
deleted theorem filter.ultrafilter_unique
modified theorem filter.Liminf_le_Limsup
modified theorem filter.liminf_const
modified theorem filter.liminf_le_limsup
modified theorem filter.limsup_const
modified theorem Liminf_eq_of_le_nhds
modified theorem Limsup_eq_of_le_nhds
modified theorem filter.tendsto.liminf_eq
modified theorem filter.tendsto.limsup_eq
modified theorem ge_of_tendsto'
modified theorem ge_of_tendsto
modified theorem le_of_tendsto_of_tendsto'
modified theorem le_of_tendsto_of_tendsto
added theorem cluster_pt.ne_bot
added theorem cluster_pt.of_le_nhds'
modified theorem cluster_pt.of_le_nhds
modified def cluster_pt
deleted theorem nhds_ne_bot
modified theorem Lim_eq
modified theorem eq_of_nhds_ne_bot
modified theorem t2_iff_nhds
added theorem tendsto_nhds_unique'
modified theorem is_compact.inter_right
modified theorem is_compact.prod
modified def is_compact
added theorem cauchy.comap'
added theorem cauchy.comap
added theorem cauchy.map
added theorem cauchy.mono'
added theorem cauchy.mono
modified def cauchy
deleted theorem cauchy_comap
deleted theorem cauchy_downwards
modified theorem cauchy_iff_exists_le_nhds
deleted theorem cauchy_map
added theorem cauchy_map_iff'
added theorem totally_bounded.image
deleted theorem totally_bounded_closure
deleted theorem totally_bounded_image