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.instHasExplicitFiniteCoproductsExtremallyDisconnectedαTopologicalSpace : CompHausLike.HasExplicitFiniteCoproducts fun (Y : TopCat) => ExtremallyDisconnected ↑Y

Equations

• Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedαTopologicalSpace = ⋯

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

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

instance Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedαTopologicalSpace : CompHausLike.HasExplicitPullbacksOfInclusions fun (Y : TopCat) => ExtremallyDisconnected ↑Y

Equations

• Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedαTopologicalSpace = ⋯