sigmaEquiv — Mathlib

English

There is a canonical equivalence between families of continuous maps and a single continuous map out of the sigma-type: (∀ i, C(X_i,A)) ≃ C((Σ i,X_i), A).

Русский

Существует каноническое эквивалентность между семействами непрерывных отображений и одним отображением на сумме: (∀ i, C(X_i,A)) ≃ C((Σ i,X_i), A).

LaTeX

$$$\\bigl((i:\\,I)\\to C(X_i,A)\\bigr) \\simeq C((\\Sigma i, X_i), A)$$$

Lean4

/-- Giving a continuous map out of a disjoint union is the same as giving a continuous map out of
each term. This is a version of `Equiv.piCurry` for continuous maps.
-/
@[simps]
def sigmaEquiv : (∀ i, C(X i, A)) ≃ C((Σ i, X i), A)
    where
  toFun := sigma
  invFun f i := f.comp (sigmaMk i)

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