mem_convexJoin — Mathlib

English

An element x belongs to convexJoin 𝕜 s t iff there exist a ∈ s and b ∈ t with x ∈ segment 𝕜 a b.

Русский

Элемент x принадлежит выпуклому соединению 𝕜 s t тогда и только тогда, когда существуют a ∈ s и b ∈ t такие, что x ∈ сегмент 𝕜 a b.

LaTeX

$$$ x \in convexJoin 𝕜 s t \;\Longleftrightarrow\; \exists a \in s, \exists b \in t, x \in segment 𝕜 a b $$$

Lean4

theorem mem_convexJoin : x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b := by simp [convexJoin]

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