English
If F is a type of maps F A1 A2 that are FunLike, ℂ-linear, and order-homomorphisms, then F is a ContinuousLinearMapClass, i.e., every f in F is a continuous linear map.
Русский
Пусть имеется множество отображений F между A1 и A2, которые линейны над ℂ и сохраняют порядок; тогда любой f из F является непрерывным линейным отображением.
LaTeX
$$$$\forall F\; \text{if } F \text{ is a FunLike } F\; A_1 \; A_2,\; \text{LinearMapClass } F \mathbb{C} A_1 A_2,\; \text{OrderHomClass } F A_1 A_2, \text{ then } F \text{ is a } ContinuousLinearMapClass F \mathbb{C} A_1 A_2.$$$$
Lean4
instance {F : Type*} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [OrderHomClass F A₁ A₂] :
ContinuousLinearMapClass F ℂ A₁ A₂ where
map_continuous
f :=
by
have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ :=
by
obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)
exact ⟨C, h⟩
exact (LinearMap.mkContinuousOfExistsBound (f : A₁ →ₗ[ℂ] A₂) hbound).continuous
