toMultilinearMap_injective — Mathlib

English

The coercion from a continuous multilinear map to its underlying multilinear map is compatible with the function-level equivalence; i.e., the coercions preserve the underlying map.

Русский

Приведение к множественному отображению сохраняет основанную функциональность и совместимо с эквивалентностью функций.

LaTeX

$$$ f.toMultilinearMap = g.toMultilinearMap \\Rightarrow f = g $$$

Lean4

theorem toMultilinearMap_injective :
    Function.Injective
      (ContinuousMultilinearMap.toMultilinearMap : ContinuousMultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₂)
  | ⟨f, hf⟩, ⟨g, hg⟩, h => by subst h; rfl

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