subset — Mathlib

English

If f and g are functions on E, and f and g are equal on S, then convexity of f on S implies convexity of g on S.

Русский

Если f и g определены на E и совпадают на S, то выпуклость f на S переносится на g.

LaTeX

$$$$ \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(S,f) \\land S\\!\\!\\!\\! \\text{EqOn}(f,g,S) \\Rightarrow \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(S,g). $$$$

Lean4

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

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