[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ CompactSpace ↑(characterSpace 𝕜 A)
[PROOFSTEP]
rw [← isCompact_iff_compactSpace]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ IsCompact (characterSpace 𝕜 A)
[PROOFSTEP]
have h : characterSpace 𝕜 A ⊆ toNormedDual ⁻¹' 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⟩⟩ : _)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ characterSpace 𝕜 A ⊆ ↑toNormedDual ⁻¹' Metric.closedBall 0 ‖1‖
[PROOFSTEP]
intro φ hφ
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ ↑toNormedDual ⁻¹' Metric.closedBall 0 ‖1‖
[PROOFSTEP]
rw [Set.mem_preimage, mem_closedBall_zero_iff]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ ‖↑toNormedDual φ‖ ≤ ‖1‖
[PROOFSTEP]
exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
h : characterSpace 𝕜 A ⊆ ↑toNormedDual ⁻¹' Metric.closedBall 0 ‖1‖
⊢ IsCompact (characterSpace 𝕜 A)
[PROOFSTEP]
exact isCompact_of_isClosed_subset (isCompact_closedBall 𝕜 0 _) CharacterSpace.isClosed h
