subset — Mathlib

English

If f is concave on a set t, and s ⊆ t, and s is convex, then f is concave on s.

Русский

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

LaTeX

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

Lean4

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

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