union_zero_isClosed — Mathlib

English

In a T2Space with continuous multiplication, the union of the character space with {0} is a closed set.

Русский

В двухместном пространстве с непрерывной умножением объединение пространства характеристик и {0} замкнуто.

LaTeX

$$$IsClosed (characterSpace 𝕜 A \\cup \\{0\\})$$$

Lean4

/-- The `characterSpace 𝕜 A` along with `0` is always a closed set in `WeakDual 𝕜 A`. -/
theorem union_zero_isClosed [T2Space 𝕜] [ContinuousMul 𝕜] : IsClosed (characterSpace 𝕜 A ∪ {0}) :=
  by
  simp only [union_zero, Set.setOf_forall]
  exact
    isClosed_iInter fun x =>
      isClosed_iInter fun y => isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)

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