instCompactSpaceElemCharacterSpaceOfProperSpace

English

If 𝕜 is a proper space and A is a normed algebra over 𝕜, then the Elem of the character space is compact.

Русский

Если 𝕜 — корректное пространство, то пространство характеров над A компактно (как множество функций).

LaTeX

$$$\text{CompactSpace}(\operatorname{characterSpace} \; 𝕜 \; A).\text{Elem}$$$

Lean4

instance [ProperSpace 𝕜] : CompactSpace (characterSpace 𝕜 A) :=
  by
  rw [← isCompact_iff_compactSpace]
  have h : characterSpace 𝕜 A ⊆ toStrongDual ⁻¹' Metric.closedBall 0 ‖(1 : A)‖ :=
    by
    intro φ hφ
    rw [Set.mem_preimage, mem_closedBall_zero_iff]
    exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)
  exact (isCompact_closedBall 𝕜 0 _).of_isClosed_subset CharacterSpace.isClosed h

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