Commit 2023-11-01 12:39 95dc8041

View on Github →

feat(Topology/Category): CompHaus, Profinite and Stonean are FinitaryExtensive. (#8012)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

Modified Mathlib/Topology/Category/Profinite/Limits.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean

added def Stonean.createsPullbacksOfOpenEmbedding

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

added def TopCat.pullbackHomeoPreimage