Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-17 18:30 3453f7a8

View on Github →

docs(order/filter/partial): add module docstring (#8620) Fix up some names:

  • core_preimage_gc -> image_core_gc
  • rtendsto_iff_le_comap -> rtendsto_iff_le_rcomap Add whitespaces around tokens

Estimated changes

deleted theorem rel.core_preimage_gc
added theorem rel.image_core_gc
modified theorem rel.mem_core
modified theorem rel.mem_preimage
modified def rel.preimage
modified theorem filter.Sup_sets_eq
modified theorem filter.comap_Sup
modified theorem filter.comap_infi
modified theorem filter.comap_ne_bot
modified theorem filter.filter_eq
modified theorem filter.inter_mem
modified theorem filter.map_supr
modified theorem filter.mem_comap
modified theorem filter.mem_infi_of_mem
modified theorem filter.mem_of_superset
modified theorem filter.mem_principal_self
modified theorem filter.mem_top_iff_forall
modified theorem filter.monotone_mem
modified theorem filter.prod_comm
modified theorem filter.seq_pure
modified theorem filter.supr_principal
modified theorem filter.supr_sets_eq
modified theorem filter.tendsto_const_pure
modified def filter.rmap
modified theorem filter.rmap_sets