English
The union of two ample sets is ample: if s and t are ample, then s ∪ t is ample.
Русский
Объединение двух ампельных множеств ампельно: если s и t ампельны, то s ∪ t ампельно.
LaTeX
$$$\forall s,t\,\big(\mathrm{AmpleSet}(s)\land \mathrm{AmpleSet}(t)\big) \\Rightarrow \mathrm{AmpleSet}(s\cup t)$$$
Lean4
/-- The union of two ample sets is ample. -/
theorem union {s t : Set F} (hs : AmpleSet s) (ht : AmpleSet t) : AmpleSet (s ∪ t) :=
by
intro x hx
rcases hx with (h | h) <;>
-- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
-- hence is also full; similarly for `t`.
[have hx := hs x h; have hx := ht x h] <;>
rw [← Set.univ_subset_iff, ← hx] <;>
apply convexHull_mono <;>
apply connectedComponentIn_mono <;>
[apply subset_union_left; apply subset_union_right]
