English
The Roth number of a union satisfies mulRothNumber(s ∪ t) ≤ mulRothNumber(s) + mulRothNumber(t).
Русский
Число Рота объединения подмножеств не превосходит суммы чисел Рота каждого из них.
LaTeX
$$$mulRothNumber(s \cup t) \le mulRothNumber(s) + mulRothNumber(t)$$$
Lean4
@[to_additive]
theorem mulRothNumber_union_le (s t : Finset α) : mulRothNumber (s ∪ t) ≤ mulRothNumber s + mulRothNumber t :=
let ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s ∪ t)
calc
mulRothNumber (s ∪ t) = #u := hcard.symm
_ = #(u ∩ s ∪ u ∩ t) := by rw [← inter_union_distrib_left, inter_eq_left.2 hus]
_ ≤ #(u ∩ s) + #(u ∩ t) := (card_union_le _ _)
_ ≤ mulRothNumber s + mulRothNumber t :=
_root_.add_le_add ((hu.mono inter_subset_left).le_mulRothNumber inter_subset_right)
((hu.mono inter_subset_left).le_mulRothNumber inter_subset_right)
