English
If hg is convex on f(S) with g, hf is convex on S with f, and hg' is monotone on f(S), then g∘f is convex on S.
Русский
Если hg выпукла на f(S) для g, hf выпукла на S для f и hg' монотонна на f(S), то g∘f выпукла на S.
LaTeX
$$$$ \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(f(S),g) \\land \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(S,f) \\land \\operatorname{MonotoneOn}_{\\mathsf{𝕜}}(g,f(S)) \\Rightarrow \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(S, g\\circ f). $$$$
Lean4
theorem comp (hg : ConvexOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) : ConvexOn 𝕜 s (g ∘ f) :=
⟨hf.1, fun _ hx _ hy _ _ ha hb hab =>
(hg' (mem_image_of_mem f <| hf.1 hx hy ha hb hab)
(hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab) <|
hf.2 hx hy ha hb hab).trans <|
hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab⟩
