Theorems · Theorem · functional analysis

SchauderBasis.finrank_range_succSub_eq_one

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {P : ℕ → X →L[𝕜] X},
  (∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n) →
    (∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x) →
      ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(SchauderBasis.succSub P n)).range = 1

Assuming that the finrank of the range of P n is n then the finrank of the range of succSub P n is 1.

Defined in

Mathlib.Analysis.Normed.Module.Bases

Cited by

1 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace