English
Characterizations of φ in span via seminorm bounds: there exist finite subset and a scalar c bounding φ by c times the supremum of the chosen seminorms.
Русский
Существуют конечное подмножество и константа c, таких что φ ≤ c · (supremum выбранных полупринорм.
LaTeX
$$$\exists s, C : Finset ι, φ.toSeminorm \le C \cdot (s.sup i (f_i.ToSeminorm))$$$
Lean4
theorem mem_span_iff_bound {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
φ ∈ Submodule.span 𝕜 (Set.range f) ↔
∃ s : Finset ι, ∃ c : ℝ≥0, φ.toSeminorm ≤ c • (s.sup fun i ↦ (f i).toSeminorm) :=
by
letI t𝕜 : TopologicalSpace 𝕜 := inferInstance
let t := ⨅ i, induced (f i) t𝕜
have : IsTopologicalAddGroup E := topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
have : WithSeminorms (fun i ↦ (f i).toSeminorm) :=
by
simp_rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_iInf, nhds_induced, map_zero, ←
comap_norm_nhds_zero (E := 𝕜), Filter.comap_comap]
rfl
rw [LinearMap.mem_span_iff_continuous]
constructor <;> intro H
· rw [Seminorm.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const] at H
rcases Seminorm.bound_of_continuous this _ H with ⟨s, C, -, hC⟩
exact ⟨s, C, hC⟩
· exact Seminorm.cont_withSeminorms_normedSpace _ this _ H
