congr — Mathlib

English

If f is convex on S and f and g agree on S, then g is convex on S.

Русский

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

LaTeX

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

Lean4

theorem congr (hf : ConvexOn 𝕜 s f) (hfg : EqOn f g s) : ConvexOn 𝕜 s g :=
  ⟨hf.1, fun x hx y hy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab⟩

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