English
The map toContinuousMap is a closed embedding when B is a topological monoid with extra structure (ContinuousMul) and T2 space.
Русский
Отображение toContinuousMap является замкнутым вложением, когда B имеет дополнительную структуру (непрерывное умножение) и является T2 пространством.
LaTeX
$$$\mathrm{IsClosedEmbedding}(\mathrm{toContinuousMap})$ при условиях [ContinuousMul B] [T2Space B].$$
Lean4
@[to_additive]
theorem isClosedEmbedding_toContinuousMap [ContinuousMul B] [T2Space B] :
IsClosedEmbedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B))
where
toIsEmbedding := isEmbedding_toContinuousMap A B
isClosed_range := by
simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall]
refine
.inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_
exact isClosed_eq (continuous_eval_const (x * y)) <| .mul (continuous_eval_const x) (continuous_eval_const y)
