mkContinuousAlternating_apply — Mathlib

English

For f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G) and C with bound H, the map mkContinuousAlternating f C H acts on m ∈ ι → E by (mkContinuousAlternating f C H) m = mkContinuous (f m) (C * ∏ i ‖m i‖) (H m). In particular, its value on m equals f m.

Русский

Пусть дано отображение f и неравенство на его норму; тогда применяемый к m ∈ ι → E отображатель mkContinuousAlternating f C H имеет значение равное f m.

LaTeX

$$$ (mkContinuousAlternating f C H) \\, m = f \\, m $$$

Lean4

@[simp]
theorem mkContinuousAlternating_apply (f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G)) {C : ℝ}
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) (m : ι → E) : ⇑(mkContinuousAlternating f C H m) = f m :=
  rfl

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