Commit 2023-02-07 15:42 22f5b710

View on Github →

feat: port Topology.StoneCech (#2147)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/StoneCech.lean

added def StoneCech

added def Ultrafilter.extend

added theorem continuous_stoneCechExtend

added theorem continuous_stoneCechUnit

added theorem continuous_ultrafilter_extend

added theorem convergent_eqv_pure

added theorem denseEmbedding_pure

added theorem denseInducing_pure

added theorem denseRange_pure

added theorem denseRange_stoneCechUnit

added theorem induced_topology_pure

added def stoneCechExtend

added theorem stoneCechExtend_extends

added def stoneCechUnit

added theorem stoneCech_hom_ext

added def ultrafilterBasis

added theorem ultrafilterBasis_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_isClosed_basic

added theorem ultrafilter_isOpen_basic

added theorem ultrafilter_pure_injective