Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 09:43 dcd90a3a

View on Github →

feat(order/filter): ultrafilter monad and the Stone-Cech compactification (#434)

feat(order/filter): simplify theory of ultrafilters slightly Introduce an alternate characterization of ultrafilters, and use it to prove ultrafilter_map and ultrafilter_pure.
chore(*): rename ultrafilter to is_ultrafilter
feat(order/filter): the ultrafilter monad
feat(analysis/topology): closure, continuous maps and T2 spaces via ultrafilters For these, first prove that a filter is the intersection of the ultrafilters containing it.
feat(analysis/topology): Normal spaces. Compact Hausdorff spaces are normal.
feat(analysis/topology/stone_cech): the Stone-Čech compactification

Estimated changes

Modified analysis/topology/continuity.lean

added theorem compact_of_closed

added theorem continuous_at_iff_ultrafilter

added theorem continuous_iff_ultrafilter

added theorem normal_of_compact_t2

Created analysis/topology/stone_cech.lean

added theorem continuous_stone_cech_extend

added theorem continuous_stone_cech_unit

added theorem continuous_ultrafilter_extend

added theorem convergent_eqv_pure

added theorem dense_embedding_pure

added def stone_cech

added def stone_cech_extend

added theorem stone_cech_extend_extends

added def stone_cech_unit

added theorem stone_cech_unit_dense

added def ultrafilter.extend

added def ultrafilter_basis

added theorem ultrafilter_basis_is_basis

added theorem ultrafilter_comap_pure_nhds

added theorem ultrafilter_converges_iff

added theorem ultrafilter_extend_eq_iff

added theorem ultrafilter_extend_extends

added theorem ultrafilter_is_closed_basic

added theorem ultrafilter_is_open_basic

added theorem ultrafilter_pure_injective

Modified analysis/topology/topological_space.lean

added theorem mem_closure_iff_ultrafilter

added theorem t2_iff_nhds

added theorem t2_iff_ultrafilter

Modified analysis/topology/uniform_space.lean

Modified order/filter.lean

modified theorem filter.exists_ultrafilter

added theorem filter.exists_ultrafilter_iff

added def filter.is_ultrafilter

modified theorem filter.le_of_ultrafilter

modified theorem filter.mem_of_finite_sUnion_ultrafilter

modified theorem filter.mem_or_compl_mem_of_ultrafilter

modified theorem filter.mem_or_mem_of_ultrafilter

added theorem filter.range_mem_map

added theorem filter.sup_of_ultrafilters

added theorem filter.tendsto_iff_ultrafilter

added def filter.ultrafilter.bind

added theorem filter.ultrafilter.eq_iff_val_le_val

added def filter.ultrafilter.map

added def filter.ultrafilter.pure

modified def filter.ultrafilter

added theorem filter.ultrafilter_bind

added theorem filter.ultrafilter_iff_compl_mem_iff_not_mem

modified theorem filter.ultrafilter_map

modified theorem filter.ultrafilter_of_spec

deleted theorem filter.ultrafilter_of_split

modified theorem filter.ultrafilter_of_ultrafilter

modified theorem filter.ultrafilter_pure

modified theorem filter.ultrafilter_ultrafilter_of

modified theorem filter.ultrafilter_unique