English
If a continuous alternating map f has a coordinate with zero norm, then the value f m has zero norm for that m.
Русский
Если f имеет координату с нулевой нормой, то f m имеет нулевую норму для соответствующего m, если f непрерывна.
LaTeX
$$$\|f\,m\| = 0 \quad\text{when } \|m_i\|=0$$$
Lean4
/-- If `f` is a continuous alternating map on `E`
and `m` is an element of `ι → E` such that one of the `m i` has norm `0`, then `f m` has norm `0`.
Note that we cannot drop the continuity assumption.
Indeed, let `ℝ₀` be a copy or `ℝ` with zero norm and indiscrete topology.
Then `f : (Unit → ℝ₀) → ℝ` given by `f x = x ()`
sends vector `1` with zero norm to number `1` with nonzero norm. -/
theorem norm_map_coord_zero (f : E [⋀^ι]→ₗ[𝕜] F) (hf : Continuous f) {m : ι → E} {i : ι} (hi : ‖m i‖ = 0) : ‖f m‖ = 0 :=
f.1.norm_map_coord_zero hf hi
