mkContinuous_coe — Mathlib

English

If a semilinear map f: E → G satisfies linearity with respect to scalar action and is bounded by a constant, then f is continuous.

Русский

Если полунаправленная линейная карта удовлетворяет линейности и ограничению, то она непрерывна.

LaTeX

$$$\forall f,\text{ if } (h_{add}, h_{smul}) \text{ and } \exists C, \forall x: E, \|f x\| \le C\|x\|, \Rightarrow \text{Continuous}(f)$$$

Lean4

@[simp, norm_cast]
theorem mkContinuous_coe (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : (f.mkContinuous C h : E →ₛₗ[σ] F) = f :=
  rfl

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