piMap — Mathlib

English

Combine a family f_i: X_i → Y_i into a single map (i ↦ X_i) → (i ↦ Y_i) by (piMap f)(a)(i) = f(i)(a_i), where a_i is the i-th component.

Русский

Объединение семейства отображений f_i: X_i → Y_i в единое отображение. Для a ∈ ∀ i X_i, (piMap f)(a)(i)=f(i)(a_i).

LaTeX

$$$\mathrm{piMap}(f) : (i:\,I) \to X_i \to (i:\,I) \to Y_i$, with $((\mathrm{piMap}(f))(a))(i) = (f(i))(a(i))$$$

Lean4

/-- Combine a collection of bundled continuous maps `C(X i, Y i)` into a bundled continuous map
`C(∀ i, X i, ∀ i, Y i)`. -/
@[simps!]
def piMap (f : ∀ i, C(X i, Y i)) : C((i : I) → X i, (i : I) → Y i) :=
  .pi fun i ↦ (f i).comp (eval i)

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