Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 15:49 675192fc

View on Github →

feat(topology): accumulation in infinite compact sets. (#16862)

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.inf_principal_eq_bot_iff_comap

added theorem filter.ne_bot_of_comap

added theorem filter.principal_eq_map_coe_top

Modified src/topology/basic.lean

Modified src/topology/constructions.lean

added theorem discrete_topology_subtype_iff

added theorem nhds_ne_subtype_eq_bot_iff

added theorem nhds_ne_subtype_ne_bot_iff

added theorem nhds_within_subtype_eq_bot_iff

Modified src/topology/order.lean

added theorem discrete_topology_iff_nhds

added theorem discrete_topology_iff_nhds_ne

Modified src/topology/separation.lean

deleted theorem discrete_topology_iff_nhds

Modified src/topology/subset_properties.lean

added theorem exists_nhds_ne_inf_principal_ne_bot

added theorem exists_nhds_ne_ne_bot

added theorem is_compact.finite