subset — Mathlib

English

If f is strictly concave on t and s ⊆ t with s convex, then f is strictly concave on s.

Русский

Если f строго конкавна на t и s ⊆ t, и s выпукло, то f строго конкавна на s.

LaTeX

$$$$ \\operatorname{StrictConcaveOn}_{\\mathsf{𝕜}}(t,f) \\land s \\subseteq t \\land \\operatorname{Convex}_{\\mathsf{𝕜}}(s) \\Rightarrow \\operatorname{StrictConcaveOn}_{\\mathsf{𝕜}}(s,f). $$$$

Lean4

theorem subset {t : Set E} (hf : StrictConcaveOn 𝕜 t f) (hst : s ⊆ t) (hs : Convex 𝕜 s) : StrictConcaveOn 𝕜 s f :=
  ⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩

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