convexBodyLT_neg_mem — Mathlib

English

If x belongs to convexBodyLT, so does -x.

Русский

Если x ∈ convexBodyLT, то и -x ∈ convexBodyLT.

LaTeX

$$$$ x \in \operatorname{convexBodyLT}(K,f) \Rightarrow -x \in \operatorname{convexBodyLT}(K,f). $$$$

Lean4

theorem convexBodyLT_neg_mem (x : mixedSpace K) (hx : x ∈ (convexBodyLT K f)) : -x ∈ (convexBodyLT K f) :=
  by
  simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply, mem_ball_zero_iff, norm_neg,
    Real.norm_eq_abs, forall_true_left, Subtype.forall, Prod.snd_neg] at hx ⊢
  exact hx

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