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.

instance Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier : CompHausLike.HasExplicitFiniteCoproducts fun (Y : TopCat) => ExtremallyDisconnected ↑Y

theorem Stonean.extremallyDisconnected_preimage {X Y Z : Stonean} {f : X ⟶ Z} (i : Y ⟶ Z) (hi : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ExtremallyDisconnected ↑(⇑(CategoryTheory.ConcreteCategory.hom i) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))

theorem Stonean.extremallyDisconnected_pullback {X Y Z : Stonean} {f : X ⟶ Z} (i : Y ⟶ Z) (hi : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ExtremallyDisconnected ↑{xy : ↑X.toTop × ↑Y.toTop | (CategoryTheory.ConcreteCategory.hom f) xy.1 = (CategoryTheory.ConcreteCategory.hom i) xy.2}

instance Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier : CompHausLike.HasExplicitPullbacksOfInclusions fun (Y : TopCat) => ExtremallyDisconnected ↑Y