English
For P in the projection subtype, the product with its complement satisfies the relation described earlier: (Pᶜ) · P = 0 and related identities.
Русский
Для P в подтипе проекций произведение с дополнением удовлетворяет ранее описанному тождеству: Pᶜ · P = 0 и сопутствующие идентичности.
LaTeX
$$Pᶜ · P = 0$$
Lean4
/-- If `f` is a continuous multilinear map on `E`
and `m` is an element of `∀ i, E i` such that one of the `m i` has norm `0`,
then `f m` has norm `0`.
Note that we cannot drop the continuity assumption because `f (m : Unit → E) = f (m ())`,
where the domain has zero norm and the codomain has a nonzero norm
does not satisfy this condition. -/
theorem norm_map_coord_zero (f : MultilinearMap 𝕜 E G) (hf : Continuous f) {m : ∀ i, E i} {i : ι} (hi : ‖m i‖ = 0) :
‖f m‖ = 0 := by
classical
rw [← inseparable_zero_iff_norm] at hi ⊢
have : Inseparable (update m i 0) m :=
inseparable_pi.2 <| (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩
simpa only [map_update_zero] using this.symm.map hf
