sub — Mathlib

English

If hs is star-convex at x in s and ht is star-convex at y in t, then x−y is star-convex at s−t.

Русский

Если hs звёздочно выпукло относительно x в s и ht звёздочно выпукло относительно y в t, то x−y звёздочно выпукло относительно s−t.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(x,s) \\wedge \\text{StarConvex}_{\\mathbb{K}}(y,t) \\Rightarrow \\text{StarConvex}_{\\mathbb{K}}(x-y, s-t)$$$

Lean4

theorem sub (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x - y) (s - t) :=
  by
  simp_rw [sub_eq_add_neg]
  exact hs.add ht.neg

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