continuous — Mathlib

English

If f is a σ12-semilinear map from M1 to M2 which is continuous as a function, then it is a continuous map from M1 to M2.

Русский

Если f — σ12-семилинейное отображение M1 в M2, и как функция оно непрерывно, то оно непрерывно как отображение между пространствами.

LaTeX

$$$\text{ContinuousLinearMap}\; (f) \Rightarrow \text{Continuous}(f\;\text{as a function})$$$

Lean4

@[continuity, fun_prop]
protected theorem continuous (f : M₁ →SL[σ₁₂] M₂) : Continuous f :=
  f.2

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