isClosedEmbedding_embedProduct — Mathlib

English

If α is a topological space with T1 separation and continuous multiplication, then embedProduct α: α → α × αᵐᵒᵖ is a closed embedding.

Русский

Если α имеет топологическое пространство с T1 и непрерывное умножение, то embedProduct α: α → α × αᵐᵒᵖ является замкнутым вложением.

LaTeX

$$$ IsClosedEmbedding (embedProduct \\alpha) $$$

Lean4

@[to_additive]
theorem isClosedEmbedding_embedProduct [T1Space α] [ContinuousMul α] : IsClosedEmbedding (embedProduct α)
    where
  toIsEmbedding := isEmbedding_embedProduct
  isClosed_range := by
    rw [range_embedProduct]
    refine .inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_) <;> fun_prop

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