instNontrivialContinuousLinearMapIdOfContinuousSMul

English

If V and W are nontrivial normed spaces over a field and ContinuousSMul holds suitably, the space of continuous linear maps from V to W is nontrivial; in particular there exists at least one nonzero continuous linear map V → L to W.

Русский

Пусть V и W — ненулевые нормированные пространства над полем; существует по крайней мере один ненулевой непрерывный линейный отображатель V → W.

LaTeX

$$$\exists T \in \mathrm{L}(V,W) \setminus \{0\}$$$

Lean4

instance (W) [AddCommGroup W] [TopologicalSpace W] [Module R W] [Nontrivial W] [ContinuousSMul R W] [Nontrivial V] :
    Nontrivial (V →L[R] W) := by
  obtain ⟨v, hv⟩ := exists_ne (0 : V)
  obtain ⟨w, hw⟩ := exists_ne (0 : W)
  obtain ⟨ψ, hψ⟩ := exists_ne_zero (R := R) hv
  exact ⟨ψ.smulRight w, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩

Похожие утверждения