subset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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