English
There is a canonical equivalence between families of continuous maps and a single continuous map out of the sigma-type, given by toFun = sigma and invFun f i = f.comp (sigmaMk i).
Русский
Существует каноническая эквивалентность между семействами непрерывных отображений и одним отображением из сигма-типа, заданная как toFun = sigma и invFun f i = f ∘ (sigmaMk i).
LaTeX
$$$(\forall i, C(X_i, A)) \simeq C((\Sigma i, X_i), A)$$$
Lean4
/-- Interpret `f : α → β` as an element of `C(α, β)`, falling back to the default value
`default : C(α, β)` if `f` is not continuous.
This is mainly intended to be used for `C(α, β)`-valued integration. For example, if a family of
functions `f : ι → α → β` satisfies that `f i` is continuous for almost every `i`, you can write
the `C(α, β)`-valued integral "`∫ i, f i`" as `∫ i, ContinuousMap.mkD (f i) 0`.
-/
noncomputable def mkD (f : α → β) (default : C(α, β)) : C(α, β) :=
open scoped Classical in if h : Continuous f then ⟨_, h⟩ else default
