instT2Space — Mathlib

English

If B is a T2 space, then the function space of continuous monoid homs is also T2.

Русский

Если B — пространство типа T2, то пространство функций непрерывных однородных гомоморфий также является T2.

LaTeX

$$$[T2Space B] \Rightarrow \; T2Space\, (\mathrm{ContinuousMonoidHom}\, A\, B).$$$

Lean4

@[to_additive]
instance [T2Space B] : T2Space (ContinuousMonoidHom A B) :=
  (isEmbedding_toContinuousMap A B).t2Space

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