Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.cocompact_eq_bot

Modification history

2022-04-06 06:48
src/topology/subset_properties.lean
feat(topology/continuous_function/zero_at_infty): add the type of continuous functions vanishing at infinity (#12907) …
Added filter.cocompact_eq_botView on Github →