English
Definition of a ring isomorphism between product spaces of finite index and a function space: continuous linear equivalence between (ι → 𝕜) and E.
Русский
Определение линейного изоморфизма между пространствами вида ι → 𝕜 и E с учётом топологии.
LaTeX
$$$\\text{piRing}(ι) : ((ι \\\\to 𝕜) \\\\to_L[𝕜] E) \\\\cong_L[𝕜] (ι \\\\to E)$$$
Lean4
/-- **Riesz's theorem**: if a closed ball with center zero of positive radius is compact in a vector
space, then the space is finite-dimensional. -/
theorem of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall (0 : E) r)) :
FiniteDimensional 𝕜 E := by
by_contra hfin
obtain ⟨R, f, Rgt, fle, lef⟩ :
∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ :=
exists_seq_norm_le_one_le_norm_sub hfin
have rRpos : 0 < r / R := div_pos rpos (zero_lt_one.trans Rgt)
obtain ⟨c, hc⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < r / R := NormedField.exists_norm_lt _ rRpos
let g := fun n : ℕ => c • f n
have A : ∀ n, g n ∈ Metric.closedBall (0 : E) r := by
intro n
simp only [g, norm_smul, dist_zero_right, Metric.mem_closedBall]
calc
‖c‖ * ‖f n‖ ≤ r / R * R := by
gcongr
· exact hc.2.le
· apply fle
_ = r := by simp [(zero_lt_one.trans Rgt).ne']
obtain
⟨x : E, _ : x ∈ Metric.closedBall (0 : E) r, φ : ℕ → ℕ, φmono : StrictMono φ, φlim : Tendsto (g ∘ φ) atTop (𝓝 x)⟩ :=
h.tendsto_subseq A
have B : CauchySeq (g ∘ φ) := φlim.cauchySeq
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → dist ((g ∘ φ) n) ((g ∘ φ) N) < ‖c‖ := Metric.cauchySeq_iff'.1 B ‖c‖ hc.1
apply lt_irrefl ‖c‖
calc
‖c‖ ≤ dist (g (φ (N + 1))) (g (φ N)) := by
conv_lhs => rw [← mul_one ‖c‖]
simp only [g, dist_eq_norm, ← smul_sub, norm_smul]
gcongr
apply lef (ne_of_gt _)
exact φmono (Nat.lt_succ_self N)
_ < ‖c‖ := hN (N + 1) (Nat.le_succ N)
