English
The join of two sets is the union of all segments joining a point from the first set to a point from the second set: convexJoin 𝕜 s t = ⋃ (x ∈ s) (y ∈ t), segment 𝕜 x y.
Русский
Соединение двух множеств — это объединение всех отрезков, соединяющих точку из первого множества с точкой из второго: convexJoin 𝕜 s t = ⋃ (x ∈ s) (y ∈ t), segment 𝕜 x y.
LaTeX
$$$ convexJoin(\,\mathbb{K}, s, t) = \bigcup_{x \in s} \bigcup_{y \in t} \operatorname{segment}(\,\mathbb{K}, x, y) $$$
Lean4
/-- The join of two sets is the union of the segments joining them. This can be interpreted as the
topological join, but within the original space. -/
def convexJoin (s t : Set E) : Set E :=
⋃ (x ∈ s) (y ∈ t), segment 𝕜 x y
