English
Equivalent reformulation: a linear functional φ lies in the span of a finite set of linear maps iff it is continuous with respect to the induced topology.
Русский
Эквивалентно: линейный функционал φ принадлежит наточному набору линейных отображений тогда и только тогда, когда он непрерывен относительно индуцированной топологии.
LaTeX
$$Iff( φ ∈ span( range f ), Continuous[ induced topology ] φ )$$
Lean4
theorem mem_span_iff_continuous {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (f i) inferInstance, inferInstance] φ :=
by
letI t𝕜 : TopologicalSpace 𝕜 := inferInstance
letI t₁ : TopologicalSpace E := ⨅ i, induced (f i) t𝕜
letI t₂ (s : Finset ι) : TopologicalSpace E := ⨅ i : s, induced (f i) t𝕜
suffices Continuous[t₁, t𝕜] φ ↔ ∃ s : Finset ι, Continuous[t₂ s, t𝕜] φ
by
simp_rw [this, ← mem_span_iff_continuous_of_finite, Submodule.span_range_eq_iSup, iSup_subtype]
rw [Submodule.mem_iSup_iff_exists_finset]
have t₁_group : @IsTopologicalAddGroup E t₁ _ := topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
have t₂_group (s : Finset ι) : @IsTopologicalAddGroup E (t₂ s) _ :=
topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
have t₁_smul : @ContinuousSMul 𝕜 E _ _ t₁ := continuousSMul_iInf fun _ ↦ continuousSMul_induced _
have t₂_smul (s : Finset ι) : @ContinuousSMul 𝕜 E _ _ (t₂ s) := continuousSMul_iInf fun _ ↦ continuousSMul_induced _
simp_rw [Seminorm.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const]
conv in Continuous _ => rw [Seminorm.continuous_iff one_pos, nhds_iInf]
conv in Continuous _ =>
rw [letI := t₂ s;
Seminorm.continuous_iff one_pos,
nhds_iInf, iInf_subtype]
rw [Filter.mem_iInf_finite]
