Commit 2024-06-28 14:12 c797e3d9

View on Github →

refactor: redefine Stone-Čech compactification (#14108) The goal is to get a universe polymorphic universal property.

Estimated changes

Modified Mathlib/Topology/StoneCech.lean

added def PreStoneCech

added theorem continuous_preStoneCechExtend

added theorem continuous_preStoneCechUnit

modified theorem continuous_stoneCechExtend

deleted theorem convergent_eqv_pure

added theorem denseRange_preStoneCechUnit

modified theorem denseRange_pure

modified theorem denseRange_stoneCechUnit

added theorem eq_if_preStoneCechUnit_eq

added theorem preStoneCechCompat

added def preStoneCechExtend

added theorem preStoneCechExtend_extends

added def preStoneCechUnit

added theorem preStoneCech_hom_ext

modified def stoneCechExtend

modified theorem stoneCechExtend_extends

modified theorem stoneCech_hom_ext