English
If f is strictly convex on S and f and g agree on S, then g is strictly convex on S.
Русский
Если f строго выпукла на S и f и g совпадают на S, то g строго выпукла на S.
LaTeX
$$$$ \\operatorname{StrictConvexOn}_{\\mathsf{𝕜}}(S,f) \\Rightarrow \\text{EqOn}(f,g,S) \\Rightarrow \\operatorname{StrictConvexOn}_{\\mathsf{𝕜}}(S,g). $$$$
Lean4
theorem comp (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s))
(hf' : s.InjOn f) : StrictConvexOn 𝕜 s (g ∘ f) :=
⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
(hg' (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab)
(hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab) <|
hf.2 hx hy hxy ha hb hab).trans <|
hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab⟩
