English
For sets s,t and points x∈s, y∈t, the diameter of s ∪ t is bounded by diam(s) + edist(x,y) + diam(t).
Русский
Для множеств s, t и точек x ∈ s, y ∈ t диаметр объединения s ∪ t ограничен суммой diam(s) + edist(x,y) + diam(t).
LaTeX
$$\operatorname{diam}(s \cup t) \le \operatorname{diam}(s) + \operatorname{edist}(x,y) + \operatorname{diam}(t) \, (x \in s, \ y \in t)$$
Lean4
/-- The diameter of a union is controlled by the diameter of the sets, and the edistance
between two points in the sets. -/
theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + edist x y + diam t :=
by
have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t := fun a ha b hb =>
calc
edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
_ ≤ diam s + edist x y + diam t :=
add_le_add (add_le_add (edist_le_diam_of_mem ha xs) le_rfl) (edist_le_diam_of_mem yt hb)
refine diam_le fun a ha b hb => ?_
rcases (mem_union _ _ _).1 ha with h'a | h'a <;> rcases (mem_union _ _ _).1 hb with h'b | h'b
·
calc
edist a b ≤ diam s := edist_le_diam_of_mem h'a h'b
_ ≤ diam s + (edist x y + diam t) := le_self_add
_ = diam s + edist x y + diam t := (add_assoc _ _ _).symm
· exact A a h'a b h'b
· have Z := A b h'b a h'a
rwa [edist_comm] at Z
·
calc
edist a b ≤ diam t := edist_le_diam_of_mem h'a h'b
_ ≤ diam s + edist x y + diam t := le_add_self
