instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier

English

TotallyDisconnectedSpace carriers have explicit pullbacks.

Русский

В картах TotallyDisconnectedSpace существуют явные произведения по обратной картинной схеме.

LaTeX

$$$\\text{HasExplicitPullbacks}(\\!\\mathrm{TotallyDisconnectedSpace}\\,\\,\\text{carrier})$$$

Lean4

instance : HasExplicitPullbacks (fun Y ↦ TotallyDisconnectedSpace Y) where
  hasProp _ _ := { hasProp := show TotallyDisconnectedSpace {_xy : _ | _} from inferInstance }

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