prodEquiv — Mathlib

English

For a family f: ι' → ContinuousMultilinearMap R M₁ (M' i), and m, pi f m j = f j m.

Русский

Для семейства f: ι' → ContinuousMultilinearMap R M₁ (M' i) и вектора m, выполняется pi f m j = f j m.

LaTeX

$$$\\pi f\\, m\\, j = f_j\\, m.$$$

Lean4

/-- `ContinuousMultilinearMap.prod` as an `Equiv`. -/
@[simps apply symm_apply_fst symm_apply_snd, simps -isSimp symm_apply]
def prodEquiv :
    (ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃) ≃ ContinuousMultilinearMap R M₁ (M₂ × M₃)
    where
  toFun f := f.1.prod f.2
  invFun
    f :=
    ((ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f,
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f)

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