Explicit limits and colimits

This file applies the general API for explicit limits and colimits in CompHausLike P (see the file Mathlib.Topology.Category.CompHausLike.Limits) to the special case of Stonean.

theorem Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier : CompHausLike.HasExplicitFiniteCoproducts fun (Y : TopCat) => ExtremallyDisconnected Y.carrier

theorem Stonean.extremallyDisconnected_preimage {X Y Z : Stonean} {f : Quiver.Hom X Z} (i : Quiver.Hom Y Z) (hi : Topology.IsOpenEmbedding (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f))) : ExtremallyDisconnected (Set.preimage (DFunLike.coe (CategoryTheory.ConcreteCategory.hom i)) (Set.range (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))).Elem

theorem Stonean.extremallyDisconnected_pullback {X Y Z : Stonean} {f : Quiver.Hom X Z} (i : Quiver.Hom Y Z) (hi : Topology.IsOpenEmbedding (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f))) : ExtremallyDisconnected (setOf fun (xy : Prod X.toTop.carrier Y.toTop.carrier) => Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) xy.fst) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom i) xy.snd)).Elem

theorem Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier : CompHausLike.HasExplicitPullbacksOfInclusions fun (Y : TopCat) => ExtremallyDisconnected Y.carrier