mkContinuous — Mathlib

English

The coe of mkContinuous equals the original f, i.e., mkContinuous produces a continuous map equal to f.

Русский

Коэффициент-отображение mkContinuous совпадает с исходным отображением f.

LaTeX

$$$ (f.mkContinuous C H) = f $$$

Lean4

/-- Construct a continuous alternating map
from a alternating map satisfying a boundedness condition. -/
def mkContinuous (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : E [⋀^ι]→L[𝕜] F :=
  { f with cont := f.continuous_of_bound C H }

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