English
If f is concave on s, it remains concave when precomposed by an affine map.
Русский
Если f конкавая на s, то f ∘ g конкавна на предобразе аффинного отображения g.
LaTeX
$$$ConcaveOn\ 𝕜\ s\ f \Rightarrow ConcaveOn 𝕜 (g^{-1}(s)) (f \circ g) \text{ for affine } g$$$
Lean4
/-- If a function is concave on `s`, it remains concave when precomposed by an affine map. -/
theorem comp_affineMap {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F} (hf : ConcaveOn 𝕜 s f) : ConcaveOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
hf.dual.comp_affineMap g