funLike — Mathlib

English

If two continuous multilinear maps into a product have equal first-coordinate projections and equal second-coordinate projections, then the maps themselves are equal.

Русский

Если два непрерывных многочленых отображения в произведение имеют одинаковые проекции на первый и второй компоненты, то сами отображения равны.

LaTeX

$$$\\text{fst}.\\circ f = \\text{fst}.\\circ g \\quad\\land\\quad \\text{snd}.\\circ f = \\text{snd}.\\circ g \\Rightarrow f = g$$$

Lean4

instance funLike : FunLike (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
    where
  coe f := f.toFun
  coe_injective' _ _ h := toMultilinearMap_injective <| MultilinearMap.coe_injective h

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