English
Given a function f:X→R and a default element of C(X,R)₀, mkD(f,default) returns f as an element of C(X,R)₀ if f is continuous and f(0)=0; otherwise it returns default.
Русский
Задавая функцию f:X→R и значение по умолчанию в C(X,R)₀, mkD(f,default) возвращает f как элемент C(X,R)₀, если f непрерывна и f(0)=0; иначе возвращает default.
LaTeX
$$$\\text{mkD } f\\ default = \\begin{cases} \\text{the element with } toFun=f \\,\\text{and } (f(0)=0) \\\\ \\text{default} \\end{cases}$$$
Lean4
/-- Interpret `f : α → β` as an element of `C(α, β)₀`, falling back to the default value
`default : C(α, β)₀` if `f` is not continuous or does not map `0` to `0`.
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 and maps `0` to `0` for almost every
`i`, you can write the `C(α, β)₀`-valued integral "`∫ i, f i`" as
`∫ i, ContinuousMapZero.mkD (f i) 0`.
-/
noncomputable def mkD [Zero X] (f : X → R) (default : C(X, R)₀) : C(X, R)₀ :=
if h : Continuous f ∧ f 0 = 0 then ⟨⟨_, h.1⟩, h.2⟩ else default
