English
For any T, F, G, U and n, the mincard of the union is bounded by the sum of the mincards: coverMincard(T, F ∪ G, U, n) ≤ coverMincard(T, F, U, n) + coverMincard(T, G, U, n).
Русский
Для любых T, F, G, U и n минкарта объединения не превосходит суммы минкарт отдельных частей.
LaTeX
$$$\operatorname{coverMincard}(T, F \cup G, U, n) \le \operatorname{coverMincard}(T, F, U, n) + \operatorname{coverMincard}(T, G, U, n)$$$
Lean4
theorem coverMincard_union_le (T : X → X) (F G : Set X) (U : Set (X × X)) (n : ℕ) :
coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n := by
classical
rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
· rw [hF, top_add]; exact le_top
rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
· rw [hG, add_top]; exact le_top
obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
rw [s.coe_union t]
exact s_cover.union t_cover
