isLinearMap_and_continuous_iff_isBoundedLinearMap

English

A map is linear and continuous if and only if it is bounded, with explicit equivalence.

Русский

Карта линейна и непрерывна тогда и только тогда, когда она ограничена, с явным эквивалентом.

LaTeX

$$$ \\text{IsLinearMap } 𝕜 f \\land \\text{Continuous } f \\iff \\text{IsBoundedLinearMap } 𝕜 f $$$

Lean4

/-- A map between normed spaces is linear and continuous if and only if it is bounded. -/
theorem isLinearMap_and_continuous_iff_isBoundedLinearMap (f : E → F) :
    IsLinearMap 𝕜 f ∧ Continuous f ↔ IsBoundedLinearMap 𝕜 f :=
  ⟨fun ⟨hlin, hcont⟩ ↦
    ContinuousLinearMap.isBoundedLinearMap ⟨⟨⟨f, IsLinearMap.map_add hlin⟩, IsLinearMap.map_smul hlin⟩, hcont⟩,
    fun h_bdd ↦ ⟨h_bdd.toIsLinearMap, h_bdd.continuous⟩⟩

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