convexBodyLT_mem — Mathlib

English

For a fixed f, the convexBodyLT is a convex set in the real vector space.

Русский

Для фиксированного f множество convexBodyLT является выпуклым в вещественном пространстве.

LaTeX

$$$\text{convexBodyLT } K f\subseteq \text{RealVectorSpace}$ is convex.$$

Lean4

theorem convexBodyLT_mem {x : K} : mixedEmbedding K x ∈ (convexBodyLT K f) ↔ ∀ w : InfinitePlace K, w x < f w := by
  simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ, forall_true_left,
    mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real, embedding_of_isReal_apply, Subtype.forall, ←
    forall₂_or_left, ← not_isReal_iff_isComplex, em, forall_true_left, norm_embedding_eq]

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