prod — Mathlib

English

The product of two continuous alternating maps is a continuous alternating map into a product space.

Русский

Произведение двух непрерывных чередующих отображений является непрерывным чередующим отображением в произведении пространств.

LaTeX

$$$ prod (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') : M [⋀^ι]→L[R] (N × N') $$$

Lean4

/-- The Cartesian product of two continuous alternating maps, as a continuous alternating map. -/
@[simps!]
def prod (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') : M [⋀^ι]→L[R] (N × N') :=
  ⟨f.1.prod g.1, (f.toAlternatingMap.prod g.toAlternatingMap).map_eq_zero_of_eq⟩

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