English
If a continuous alternating map satisfies a shell-bounded inequality, it satisfies the global bound.
Русский
Если непрерывное чередующееся отображение удовлетворяет оболочному неравенству, оно удовлетворяет всемогущему пределу.
LaTeX
$$$\|f m\| \le C \prod_i \|m_i\|$ для всех m$$
Lean4
/-- If a continuous alternating map in finitely many variables on normed spaces
satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`
on a shell `ε / ‖c‖ < ‖m i‖ < ε` for some positive number `ε` and an elements `c : 𝕜`, `1 < ‖c‖`,
then it satisfies this inequality for all `m`.
If the domain is a Hausdorff space, then the continuity assumption is redundant,
see `bound_of_shell` below. -/
theorem bound_of_shell_of_continuous (f : E [⋀^ι]→ₗ[𝕜] F) (hfc : Continuous f) {ε : ℝ} {C : ℝ} (hε : 0 < ε) {c : 𝕜}
(hc : 1 < ‖c‖) (hf : ∀ m : ι → E, (∀ i, ε / ‖c‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m : ι → E) :
‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
f.1.bound_of_shell_of_continuous hfc (fun _ ↦ hε) (fun _ ↦ hc) hf m
