English
Let C be a set system closed under finite unions (a semiring). Let m be an additive content on C. If J is a finite collection of sets with each member in C, and t is in C with t contained in the union of all sets in J, then m(t) is bounded above by the sum of m over the members of J.
Русский
Пусть C—пакет множеств, замкнутый при ограниченной на конечную объединение (полукольцо). Пусть m — аддитивное содержимое на C. Пусть J — конечное подмножество (финсет) множеств, каждое из которых принадлежит C, и t ∈ C с включением t в объединение ⋃J. Тогда m(t) ≤ ∑_{u∈J} m(u).
LaTeX
$$$m(t) \le \sum_{u \in J} m(u) \,.$$$
Lean4
theorem addContent_le_sum_of_subset_sUnion {m : AddContent C} (hC : IsSetSemiring C) {J : Finset (Set α)}
(h_ss : ↑J ⊆ C) (ht : t ∈ C) (htJ : t ⊆ ⋃₀ ↑J) : m t ≤ ∑ u ∈ J, m u := by
-- we can't apply `addContent_mono` and `addContent_sUnion_le_sum` because `⋃₀ ↑J` might not
-- be in `C`
classical
let Jt := J.image (fun u ↦ t ∩ u)
have ht_eq : t = ⋃₀ Jt :=
by
rw [coe_image, sUnion_image, ← inter_iUnion₂, inter_eq_self_of_subset_left]
rwa [← sUnion_eq_biUnion]
rw [ht_eq]
refine (addContent_sUnion_le_sum hC Jt ?_ ?_).trans ?_
· intro s
simp only [Jt, coe_image, Set.mem_image, mem_coe, forall_exists_index, and_imp]
rintro u hu rfl
exact hC.inter_mem _ ht _ (h_ss hu)
· rwa [← ht_eq]
· refine (Finset.sum_image_le_of_nonneg fun _ _ ↦ zero_le _).trans (sum_le_sum fun u hu ↦ ?_)
exact addContent_mono hC (hC.inter_mem _ ht _ (h_ss hu)) (h_ss hu) inter_subset_right
