eq_prod_iff — Mathlib

English

If two continuous multilinear maps f,g into a product have equal first-projections and equal second-projections, then f=g.

Русский

Если две непрерывные мультилинейные карты f,g в произведение имеют равные проекции fst и snd, тогда они равны.

LaTeX

$$$\text{prod_ext}\; (h_1,h_2) : (\forall f,g, (\text{fst}.\circ f)=(\text{fst}.\circ g) \land (\text{snd}.\circ f)=(\text{snd}.\circ g) \Rightarrow f=g$$$

Lean4

theorem eq_prod_iff {f : ContinuousMultilinearMap R M₁ (M₂ × M₃)} {g : ContinuousMultilinearMap R M₁ M₂}
    {h : ContinuousMultilinearMap R M₁ M₃} :
    f = g.prod h ↔
      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f = g ∧
        (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f = h :=
  prod_ext_iff

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