Theorems · Theorem · functional analysis

LinearMap.mem_span_iff_bound

∀ {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜),
  φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i => (f i).toSeminorm

Defined in

Mathlib.Analysis.LocallyConvex.WeakDual

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModule