Commit 2023-10-25 20:48 57e4e03d

View on Github →

feat(Filter): lemmas from Mandelbrot connectedness project (#7913)

  • Add Filter.frequently_iff_neBot and Filter.frequently_mem_iff_neBot.
  • Drop some implicit arguments that are available from variable.
  • Add Filter.disjoint_prod and Filter.frequently_prod_and.
  • Swap Filter.le_prod with Filter.tendsto_prod_iff' to use the latter in the proof of the former. Co-Authored-By: @girving

Estimated changes

modified theorem Filter.NeBot.prod
modified theorem Filter.Tendsto.prod_mk
modified theorem Filter.bot_prod
added theorem Filter.disjoint_prod
modified theorem Filter.eventually_prod_iff
modified theorem Filter.inf_prod
modified theorem Filter.map_swap4_prod
modified theorem Filter.mem_prod_iff_left
modified theorem Filter.mem_prod_iff_right
modified theorem Filter.mem_prod_principal
modified theorem Filter.mem_prod_top
modified theorem Filter.prod_bot
modified theorem Filter.prod_eq
modified theorem Filter.prod_eq_bot
modified theorem Filter.prod_inf
modified theorem Filter.prod_mem_prod
modified theorem Filter.prod_mem_prod_iff
modified theorem Filter.prod_neBot
modified theorem Filter.prod_pure
modified theorem Filter.prod_top
modified theorem Filter.tendsto_fst
modified theorem Filter.tendsto_prodAssoc
modified theorem Filter.tendsto_prod_iff'
modified theorem Filter.tendsto_prod_swap
modified theorem Filter.tendsto_snd
modified theorem Filter.tendsto_swap4_prod