extremallyDisconnected_pullback — Mathlib

English

The pullback of an extremally disconnected map along an open embedding is extremally disconnected.

Русский

Диагональный (pullback) граф экстремально разобщенной карты по открывающему вложению сохраняет свойство экстремально разобщенности.

LaTeX

$$$\operatorname{ExtremallyDisconnected}\bigl{\{xy:\;X\times Y \mid f(x)=i(y)\}\bigr}$$$

Lean4

theorem extremallyDisconnected_pullback : ExtremallyDisconnected {xy : X × Y | f xy.1 = i xy.2} :=
  have := extremallyDisconnected_preimage i hi
  let e := (TopCat.pullbackHomeoPreimage i i.hom.2 f hi.isEmbedding).symm
  let e' : {xy : X × Y | f xy.1 = i xy.2} ≃ₜ {xy : Y × X | i xy.1 = f xy.2} := by
    exact
      TopCat.homeoOfIso
        ((TopCat.pullbackIsoProdSubtype f i).symm ≪≫ pullbackSymmetry _ _ ≪≫ (TopCat.pullbackIsoProdSubtype i f))
  extremallyDisconnected_of_homeo (e.trans e'.symm)

Похожие утверждения