compContinuousAlternatingMap_coe — Mathlib

English

Let g: N →L[R] N' be a continuous linear map and f: M [⋀^ι]→L[R] N a continuous alternating map. Then the postcomposition g ∘ f is a continuous alternating map, and its action on any argument m agrees with the pointwise composition g ∘ f(m) = g(f(m)).

Русский

Пусть g: N →L[R] N' — непрерывное линейное отображение и f: M [⋀^ι]→L[R] N — непрерывная чередующая карта. Тогда посткомпозиции g ∘ f образует непрерывную чередующую карту, и её действие на любой аргумент m удовлетворяет (g ∘ f)(m) = g(f(m)).

LaTeX

$$$\forall g: N \to_L[R] N',\ \forall f: M [\⋀^ι] \toL[R] N,\ (g \circ f) (m) = g(f(m))\ \text{for all } m.$$$

Lean4

@[simp]
theorem _root_.ContinuousLinearMap.compContinuousAlternatingMap_coe (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) :
    ⇑(g.compContinuousAlternatingMap f) = g ∘ f :=
  rfl

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