English
Compose a left function g: β→γ with a compactly supported f: α→β to obtain a compactly supported map α→γ; when g(0)=0, the result is g ∘ f, otherwise it is 0; with the appropriate compact support proof.
Русский
Слева функцию g: β→γ композиционно соотносим с компактно поддерживаемым f: α→β, образуя отображение α→γ с компактной опорой; если g(0)=0, результат равен g∘f, иначе 0; с соответствующим доказательством компактной опоры.
LaTeX
$$$ \text{compLeft}(g,f) = \begin{cases} g \circ f, & g(0)=0 \\ 0, & \text{иначе} \end{cases} $$$
Lean4
/-- Composition of a continuous function `f` with compact support with another continuous function
`g` sending `0` to `0` from the left yields another continuous function `g ∘ f` with compact
support.
If `g` doesn't send `0` to `0`, `f.compLeft g` defaults to `0`. -/
noncomputable def compLeft (g : C(β, γ)) (f : C_c(α, β)) : C_c(α, γ)
where
toContinuousMap := by classical exact if g 0 = 0 then g.comp f else 0
hasCompactSupport' := by
split_ifs with hg
· exact f.hasCompactSupport'.comp_left hg
· exact .zero
