Kadec–Klee property

TheoremKadec–Klee property, all-functionals form#✓fully proved

Let \(E\) be a uniformly convex real normed space, let \((u_n)\) be a sequence in \(E\) and let \(x \in E\). If \(f(u_n) \to f(x)\) for every continuous linear functional \(f \colon E \to \mathbb{R}\) and \(\|u_n\| \to \|x\|\), then \(u_n \to x\) in norm.

theorem tendsto_of_forall_tendsto_and_tendsto_norm {u : ℕ → E} {x : E}
    (hweak : ∀ f : StrongDual ℝ E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x)))
    (hnorm : Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)) :
    Tendsto u atTop (𝓝 x)

Used by 2

Used byKadec–Klee iff, all-functionals form · Kadec–Klee property, weak-topology form

TheoremKadec–Klee property, weak-topology form#✓fully proved

Let \(E\) be a uniformly convex real normed space, let \((u_n)\) be a sequence in \(E\) and let \(x \in E\). If \(u_n \to x\) in the weak topology of \(E\) (the topology induced by the continuous linear functionals \(E \to \mathbb{R}\)) and \(\|u_n\| \to \|x\|\), then \(u_n \to x\) in norm.

theorem tendsto_of_tendsto_weakSpace_and_tendsto_norm {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace ℝ E (u n)) atTop (𝓝 (toWeakSpace ℝ E x)))
    (hnorm : Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)) :
    Tendsto u atTop (𝓝 x)

Uses 2 · Used by 1

Proof usesKadec–Klee property, all-functionals form · Weak convergence gives convergence under every functional

Used byKadec–Klee iff, weak-topology form

TheoremKadec–Klee iff, all-functionals form#✓fully proved

Let \(E\) be a uniformly convex real normed space, let \((u_n)\) be a sequence in \(E\) and let \(x \in E\). Then \(u_n \to x\) in norm if and only if \(f(u_n) \to f(x)\) for every continuous linear functional \(f \colon E \to \mathbb{R}\) and \(\|u_n\| \to \|x\|\).

theorem tendsto_iff_forall_tendsto_and_tendsto_norm {u : ℕ → E} {x : E} :
    Tendsto u atTop (𝓝 x) ↔
      (∀ f : StrongDual ℝ E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) ∧
        Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)

Uses 1

Proof usesKadec–Klee property, all-functionals form

TheoremKadec–Klee iff, weak-topology form#✓fully proved

Let \(E\) be a uniformly convex real normed space, let \((u_n)\) be a sequence in \(E\) and let \(x \in E\). Then \(u_n \to x\) in norm if and only if \(u_n \to x\) in the weak topology of \(E\) (the topology induced by the continuous linear functionals \(E \to \mathbb{R}\)) and \(\|u_n\| \to \|x\|\).

theorem tendsto_iff_tendsto_weakSpace_and_tendsto_norm {u : ℕ → E} {x : E} :
    Tendsto u atTop (𝓝 x) ↔
      Tendsto (fun n => toWeakSpace ℝ E (u n)) atTop
        (𝓝 (toWeakSpace ℝ E x)) ∧
        Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)

Uses 2

Proof usesKadec–Klee property, weak-topology form · Convergence under every functional gives weak convergence

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.