precomp — Mathlib

English

"Precomposition" as a continuous map between dependent types: φ : ι → I induces a continuous map from (i:I → X_i) to (i:ι → X_(φ i)).

Русский

"Предпосложение" как непрерывное отображение между зависимыми типами: φ : ι → I задаёт непрерывное отображение от (i:I → X_i) к (i:ι → X_(φ i)).

LaTeX

$$$\mathrm{precomp}_{\varphi} : C((i:I) \to X_i, (i:ι) \to X_{\varphi i})$ with $\mathrm{toFun}(h)(i) = h(\varphi i)$$$

Lean4

/-- "Precomposition" as a continuous map between dependent types. -/
def precomp {ι : Type*} (φ : ι → I) : C((i : I) → X i, (i : ι) → X (φ i)) :=
  ⟨_, Pi.continuous_precomp' φ⟩

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