instCompactSpace — Mathlib

English

If B is a compact space, along with discreteness of A and suitable continuity assumptions, then ContinuousMonoidHom A B is a compact space.

Русский

Если B компактно, и A дискретно, при прочих условия непрерывности, то ContinuousMonoidHom A B компактно.

LaTeX

$$$[CompactSpace B] \Rightarrow \mathrm{CompactSpace}( \mathrm{ContinuousMonoidHom} A B).$$$

Lean4

@[to_additive]
instance [CompactSpace B] : CompactSpace (A →ₜ* B) :=
  ContinuousMonoidHom.isClosedEmbedding_coe.compactSpace

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