Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 09:59 e21dc7a9

View on Github →

feat(topology/subset_properties): define filter.cocompact (#4666) The filter of complements to compact subsets.

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem continuous.norm

added theorem tendsto_norm_cocompact_at_top

Modified src/data/set/basic.lean

added theorem set.nonempty_insert

Modified src/topology/algebra/ordered.lean

added theorem continuous.exists_forall_ge

added theorem continuous.exists_forall_le

Modified src/topology/metric_space/basic.lean

added theorem tendsto_dist_left_cocompact_at_top

added theorem tendsto_dist_right_cocompact_at_top

Modified src/topology/separation.lean

Modified src/topology/subset_properties.lean

added def filter.cocompact

added theorem filter.has_basis_cocompact

added theorem filter.mem_cocompact'

added theorem filter.mem_cocompact

added theorem is_compact.compl_mem_cocompact

added theorem is_compact.insert