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 ⇑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}