mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(order/filter,topology/instances/nnreal): upgrade some lemmas to `iff`

Open urkud opened this issue 2 years ago • 1 comments

  • Add codisjoint.inf_left_sup_inf_right and is_compl.le_inf_sup_inf.
  • Add filter.comap_ite, filter.comap_max, and filter.tendsto_ite.
  • Add real.map_to_nnreal_at_top, real.comap_to_nnreal_at_top, and real.tendsto_to_nnreal_at_top_iff.
  • Rename tendsto_real_to_nnreal to filter.tendsto.real_to_nnreal so that it can be used with dot notation.
  • Add ennreal.tendsto_of_real_nhds_top.

I'm cleaning up old local branches. I don't remember why I wanted to have these lemmas but IMHO upgrading from implications to iffs is a good thing.

Open in Gitpod

urkud avatar May 07 '23 19:05 urkud