pi — Mathlib · SciLib

English

Abbreviation for product of continuous maps: if f(i) : A → X_i for each i, then (pi f)(a) is the tuple (f(i)(a))_i.

Русский

Сокращение для произведения непрерывных отображений: если f_i: A → X_i для каждого i, то (π f)(a) = (f_i(a))_i.

LaTeX

$$$\pi: (\forall i, C(A, X_i)) \to C(A, \forall i, X_i),\qquad (\pi f)(a)(i) = f(i)(a)$$$

Lean4

/-- Abbreviation for product of continuous maps, which is continuous -/
def pi (f : ∀ i, C(A, X i)) : C(A, ∀ i, X i) where toFun (a : A) (i : I) := f i a

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