Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-08 08:46 ffa6d699

View on Github →

feat(*): has_mem (set α) (filter α) (#799)

Estimated changes

modified theorem filter.realizer.mem_sets
modified def measure_theory.all_ae
modified theorem filter.bind_mono
modified theorem filter.congr_sets
modified theorem filter.empty_in_sets_eq_bot
modified theorem filter.image_mem_map
modified theorem filter.inf_principal_eq_bot
modified theorem filter.infi_sets_induct
modified theorem filter.inter_mem_sets
modified theorem filter.le_def
modified theorem filter.le_map
modified theorem filter.le_principal_iff
modified theorem filter.map_comap
modified theorem filter.map_cong
modified theorem filter.map_inf'
modified theorem filter.mem_at_top
modified theorem filter.mem_bot_sets
modified theorem filter.mem_comap_sets
modified theorem filter.mem_inf_sets_of_left
added theorem filter.mem_infi
added theorem filter.mem_infi_finite
modified theorem filter.mem_infi_sets
modified theorem filter.mem_map
modified theorem filter.mem_map_sets_iff
modified theorem filter.mem_principal_self
modified theorem filter.mem_principal_sets
modified theorem filter.mem_pure
modified theorem filter.mem_pure_iff
modified theorem filter.mem_sets_of_neq_bot
modified theorem filter.mem_sets_of_superset
modified theorem filter.mem_top_sets
modified theorem filter.monotone_mem_sets
modified theorem filter.mp_sets
modified theorem filter.preimage_mem_comap
modified theorem filter.range_mem_map
modified theorem filter.univ_mem_sets'
modified theorem filter.univ_mem_sets
modified def filter.mem_pmap
modified theorem exists_nhds_split4
modified theorem exists_nhds_split
modified theorem exists_nhds_split_inv
modified theorem ge_mem_nhds
modified theorem gt_mem_nhds
modified theorem le_mem_nhds
modified theorem lt_mem_nhds
modified theorem mem_nhds_orderable_dest
modified theorem is_open_iff_mem_nhds
modified theorem mem_closure_iff_nhds
modified theorem mem_of_nhds
modified theorem map_nhds_subtype_val_eq
modified theorem ennreal.coe_range_mem_nhds
modified theorem metric.ball_mem_nhds
modified theorem metric.mem_nhds_iff
modified theorem emetric.ball_mem_nhds
modified theorem emetric.mem_nhds_iff
modified theorem map_nhds_induced_eq
modified theorem compl_singleton_mem_nhds
modified theorem nhds_is_closed
modified theorem comp_mem_uniformity_sets
modified theorem comp_symm_of_uniformity
modified theorem interior_mem_uniformity
added theorem mem_map_sets_iff'
modified theorem mem_uniformity_is_closed
modified theorem nhdset_of_mem_uniformity
modified theorem refl_mem_uniformity
modified theorem symm_of_uniformity