coe_mkContinuous

Mathlib.Analysis.NormedSpace.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#AlternatingMap.coe_mkContinuous

English

If f = f1 and C = C1, then f.mkContinuous C H = f1.mkContinuous C1 H.

Русский

Если f = f1 и C = C1, то f.mkContinuous C H = f1.mkContinuous C1 H.

LaTeX

$$$f = f_1 \Rightarrow f.mkContinuous C H = f_1.mkContinuous C_1 H$$$

Lean4

@[simp]
theorem coe_mkContinuous (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    (f.mkContinuous C H : (ι → E) → F) = f :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru