neg — Mathlib

English

If s is star-convex at x, then −s is star-convex at −x.

Русский

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

LaTeX

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

Lean4

theorem neg (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (-x) (-s) :=
  by
  rw [← image_neg_eq_neg]
  exact hs.is_linear_image IsLinearMap.isLinearMap_neg

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