Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 12:26 3f868fab

View on Github →

feat(filter, topology): cluster_pt and principal notation, redefine compactness (#3160) This PR implements what is discussed in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Picking.20sides. It introduces a notation for filter.principal, defines cluster_pt and uses it to redefine compactness in a way which makes the library more consistent by always putting the neighborhood filter on the left, as in the description of closures and nhds_within.

Estimated changes

modified def filter.at_bot
modified def filter.at_top
modified theorem filter.comap_principal
modified theorem filter.inf_principal
modified theorem filter.inf_principal_eq_bot
modified theorem filter.is_compl_principal
modified theorem filter.le_principal_iff
modified theorem filter.mem_principal_self
modified theorem filter.mem_principal_sets
modified theorem filter.mem_sets_of_eq_bot
modified theorem filter.monotone_principal
modified theorem filter.principal_empty
modified theorem filter.principal_eq_bot_iff
modified theorem filter.principal_eq_iff_eq
modified theorem filter.principal_mono
modified theorem filter.principal_ne_bot_iff
modified theorem filter.principal_univ
modified theorem filter.pure_eq_principal
modified theorem filter.sup_principal
modified theorem filter.supr_principal
modified def is_extr_on
modified def is_max_on
modified def is_min_on
modified theorem filter.lift_principal2
modified theorem filter.le_of_ultrafilter
modified theorem filter.is_bounded_principal
added theorem closure_eq_cluster_pts
deleted theorem closure_eq_nhds
added theorem cluster_pt.mono
added theorem cluster_pt.of_le_nhds
added theorem cluster_pt.of_nhds_le
added def cluster_pt
added theorem cluster_pt_of_inf_left
modified theorem interior_eq_nhds
modified theorem is_closed_iff_nhds
modified theorem is_open_iff_nhds
added def map_cluster_pt
added theorem map_cluster_pt_iff
added theorem map_cluster_pt_of_comp
modified def nhds
modified theorem nhds_def
modified theorem nhds_le_of_le
modified def nhds_within
modified theorem ennreal.nhds_of_ne_top
modified theorem ennreal.nhds_top
modified theorem ennreal.nhds_zero
modified theorem metric.uniformity_edist
modified theorem emetric.nhds_eq
modified def compact
modified theorem refl_le_uniformity
modified def is_complete