instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier

English

There are explicit finite coproducts for TotallyDisconnectedSpace carriers.

Русский

Существуют явные конечные копроизведения для носителей TotallyDisconnectedSpace.

LaTeX

$$$\\text{HasExplicitFiniteCoproducts}(\\mathrm{TotallyDisconnectedSpace}\\;X)$$$

Lean4

instance : HasExplicitFiniteCoproducts.{w, u} (fun Y ↦ TotallyDisconnectedSpace Y) where
  hasProp _ := { hasProp := show TotallyDisconnectedSpace (Σ (_a : _), _) from inferInstance }

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