comp_affineMap — Mathlib

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

Похожие утверждения