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.extremallyDisconnected_preimage
{X Y Z : Stonean}
{f : X ⟶ Z}
(i : Y ⟶ Z)
(hi : Topology.IsOpenEmbedding ⇑(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}