comp_linearMap — Mathlib

English

If f is concave on s, then f ∘ g is concave on the preimage of s under a linear map g.

Русский

Если f конкавна на s, то f ∘ g конкавна на прообразе s под линейным отображением g.

LaTeX

$$$\text{If } f \text{ is concave on } s, \text{ then } f\circ g \text{ is concave on } g^{-1}(s)$$$

Lean4

/-- If `f` is concave on `s`, so is `(g ∘ f)` on `g ⁻¹' s` for a linear `g`. -/
theorem comp_linearMap {f : F → β} {s : Set F} (hf : ConcaveOn 𝕜 s f) (g : E →ₗ[𝕜] F) : ConcaveOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
  hf.dual.comp_linearMap g

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