piEquiv — Mathlib

English

Equality of a product map with a pair is determined by the equality of its fst and snd projections.

Русский

Равенство отображения в произведение определяет равенство его проекций fst и snd.

LaTeX

$$$f = g.prod h \iff (\text{fst} \circ f) = g \land (\text{snd} \circ f) = h$$$

Lean4

/-- `ContinuousMultilinearMap.pi` as an `Equiv`. -/
@[simps]
def piEquiv {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)]
    [∀ i, Module R (M' i)] : (∀ i, ContinuousMultilinearMap R M₁ (M' i)) ≃ ContinuousMultilinearMap R M₁ (∀ i, M' i)
    where
  toFun := ContinuousMultilinearMap.pi
  invFun f i := (ContinuousLinearMap.proj i : _ →L[R] M' i).compContinuousMultilinearMap f

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