Theorem ultrafilter_pure_injective

Modification history

2025-08-16 00:47
Mathlib/Topology/Compactification/StoneCech.lean
chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (#28436)
Deleted ultrafilter_pure_injectiveView on Github →
2023-02-07 15:42
Mathlib/Topology/StoneCech.lean
feat: port Topology.StoneCech (#2147)
Added ultrafilter_pure_injectiveView on Github →