Theorems · Theorem · functional analysis

Seminorm.bound_of_shell_sup

∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : ι → Seminorm 𝕜 E) (s : Finset ι) (q : Seminorm 𝕜 E) {ε : ℝ} {C : NNReal},
  0 < ε →
    ∀ {c : 𝕜},
      1 < ‖c‖ →
        (∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x) →
          ∀ {x : E}, (∃ j ∈ s, (p j) x ≠ 0) → q x ≤ (C • s.sup p) x

Defined in

Mathlib.Analysis.Seminorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldAddCommGroupModule