toContinuousMultilinearMap_injective

English

The map from ContinuousAlternatingMap to ContinuousMultilinearMap is injective.

Русский

Отображение ContinuousAlternatingMap → ContinuousMultilinearMap инъективно.

LaTeX

$$$ \\text{Injective}(\\mathrm{toContinuousMultilinearMap}: \\mathrm{ContinuousAlternatingMap}\\ M\\ [⋀^ι]\\to L[R](\\text{...}) \\to \\mathrm{ContinuousMultilinearMap}\\ ) $$$

Lean4

theorem toContinuousMultilinearMap_injective :
    Injective
      (ContinuousAlternatingMap.toContinuousMultilinearMap :
        M [⋀^ι]→L[R] N → ContinuousMultilinearMap R (fun _ : ι => M) N)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

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