Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-01 18:32 ba197e48

View on Github →

feat(order/filter/*,topology/noetherian_space): add lemmas about cofinite (#16498)

A filter is disjoint with cofinite iff there exists a finite set that belongs to this filter.
An ultrafilter is either less than or equal to cofinite, or is equal to pure a for some a.
Any type with cofinite topology is a Noetherian (hence, is a compact) space.

Estimated changes

Modified src/order/filter/cofinite.lean

added theorem filter.disjoint_cofinite_left

added theorem filter.disjoint_cofinite_right

modified theorem filter.le_cofinite_iff_compl_singleton_mem

modified theorem filter.le_cofinite_iff_eventually_ne

Modified src/order/filter/ultrafilter.lean

added theorem ultrafilter.disjoint_iff_not_le

modified theorem ultrafilter.eq_pure_of_finite

modified theorem ultrafilter.eq_pure_of_finite_mem

added theorem ultrafilter.inf_ne_bot_iff

added theorem ultrafilter.le_cofinite_or_eq_pure

added theorem ultrafilter.le_sup_iff

modified theorem ultrafilter.union_mem_iff

Modified src/topology/noetherian_space.lean