convexBodyLT'_neg_mem — Mathlib

English

Membership in convexBodyLT' K f w0 is equivalent to a conjunction of inequalities and component conditions.

Русский

Принадлежность convexBodyLT' эквивалентна сочетанию неравенств и условийComponent.

LaTeX

$$$$ x \in \operatorname{convexBodyLT'}(K,f,w_0) \iff (\forall w, w \neq w_0, w x < f w) \land (|(w_0).embedding(x).re| < 1) \land (|(w_0).embedding(x).im| < (f w_0)^2). $$$$

Lean4

theorem convexBodyLT'_neg_mem (x : mixedSpace K) (hx : x ∈ convexBodyLT' K f w₀) : -x ∈ convexBodyLT' K f w₀ :=
  by
  simp only [Set.mem_prod, Set.mem_pi, Set.mem_univ, mem_ball, dist_zero_right, Real.norm_eq_abs, true_implies,
    Subtype.forall, Prod.fst_neg, Pi.neg_apply, norm_neg, Prod.snd_neg] at hx ⊢
  convert hx using 3
  split_ifs <;> simp

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