pi — Mathlib · SciLib

English

The evaluation of the pi-construction at an argument equals evaluating at that index: (pi f) m j = f j m.

Русский

Оценка конструкции Pi по аргументу равна оценке на соответствующем индексе: (pi f) m j = f j m.

LaTeX

$$$ pi\\ f\\ m\\ j = f\\ j\\ m $$$

Lean4

/-- Combine a family of continuous alternating maps with the same domain and codomains `M' i` into a
continuous alternating map taking values in the space of functions `Π i, M' i`. -/
def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
    (f : ∀ i, M [⋀^ι]→L[R] M' i) : M [⋀^ι]→L[R] ∀ i, M' i :=
  ⟨ContinuousMultilinearMap.pi fun i => (f i).1, (AlternatingMap.pi fun i => (f i).toAlternatingMap).map_eq_zero_of_eq⟩

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