addContent_union' — Mathlib

English

A refined version of sUnion for disjoint unions under subset assumptions.

Русский

Уточнённая версия разборного объединения над дизъюнктными частями при предпосылках подмножеств.

LaTeX

$$m( s ∪ t ) = m(s) + m(t) under disjointness and subset hypotheses$$

Lean4

theorem addContent_union' (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_dis : Disjoint s t) : m (s ∪ t) = m s + m t :=
  by
  by_cases hs_empty : s = ∅
  · simp only [hs_empty, Set.empty_union, addContent_empty, zero_add]
  classical
  have h := addContent_sUnion (m := m) (I := { s, t }) ?_ ?_ ?_
  rotate_left
  · simp only [coe_pair, Set.insert_subset_iff, hs, ht, Set.singleton_subset_iff, and_self_iff]
  · simp only [coe_pair, Set.pairwiseDisjoint_insert, pairwiseDisjoint_singleton, mem_singleton_iff, Ne, id, forall_eq,
      true_and]
    exact fun _ => h_dis
  · simp only [coe_pair, sUnion_insert, sUnion_singleton]
    exact hst
  convert h
  · simp only [coe_pair, sUnion_insert, sUnion_singleton]
  · rw [sum_insert, sum_singleton]
    simp only [Finset.mem_singleton]
    refine fun hs_eq_t => hs_empty ?_
    rw [← hs_eq_t] at h_dis
    exact Disjoint.eq_bot_of_self h_dis

Похожие утверждения