English
There exists a finite disjoint family J ⊆ C such that s \\ ⋃₀ I = ⋃₀ J.
Русский
Существует конечное попарно непересекающееся семейство J ⊆ C такое, что s \\, ⋃₀ I = ⋃₀ J.
LaTeX
$$$$ \\exists J : Finset (Set α), \\uparrow J ⊆ C \\wedge J.toSet.PairwiseDisjoint id \\wedge s \\\\setminus ⋃_0 I = ⋃_0 J $$$$
Lean4
/-- In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`, there is a
finite set of sets in `C` whose union is `s \ ⋃₀ I`.
See `IsSetSemiring.disjointOfDiffUnion` for a definition that gives such a set. -/
theorem exists_disjoint_finset_diff_eq (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
∃ J : Finset (Set α), ↑J ⊆ C ∧ PairwiseDisjoint (J : Set (Set α)) id ∧ s \ ⋃₀ I = ⋃₀ J := by
classical
induction I using Finset.induction with
| empty =>
simp only [coe_empty, sUnion_empty, diff_empty]
refine ⟨{ s }, singleton_subset_set_iff.mpr hs, ?_⟩
simp only [coe_singleton, pairwiseDisjoint_singleton, sUnion_singleton, and_self_iff]
| insert t I' _ h => ?_
rw [coe_insert] at hI
have ht : t ∈ C := hI (Set.mem_insert _ _)
obtain ⟨J, h_ss, h_dis, h_eq⟩ := h ((Set.subset_insert _ _).trans hI)
let Ju : ∀ u ∈ C, Finset (Set α) := fun u hu ↦ hC.disjointOfDiff hu ht
have hJu_subset : ∀ (u) (hu : u ∈ C), ↑(Ju u hu) ⊆ C :=
by
intro u hu x hx
exact hC.subset_disjointOfDiff hu ht hx
have hJu_disj : ∀ (u) (hu : u ∈ C), (Ju u hu : Set (Set α)).PairwiseDisjoint id := fun u hu ↦
hC.pairwiseDisjoint_disjointOfDiff hu ht
have hJu_sUnion : ∀ (u) (hu : u ∈ C), ⋃₀ (Ju u hu : Set (Set α)) = u \ t := fun u hu ↦ hC.sUnion_disjointOfDiff hu ht
have hJu_disj' :
∀ (u) (hu : u ∈ C) (v) (hv : v ∈ C) (_h_dis : Disjoint u v),
Disjoint (⋃₀ (Ju u hu : Set (Set α))) (⋃₀ ↑(Ju v hv)) :=
by
intro u hu v hv huv_disj
rw [hJu_sUnion, hJu_sUnion]
exact disjoint_of_subset Set.diff_subset Set.diff_subset huv_disj
let J' : Finset (Set α) := Finset.biUnion (Finset.univ : Finset J) fun u ↦ Ju u (h_ss u.prop)
have hJ'_subset : ↑J' ⊆ C := by
intro u
simp only [J', univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true, mem_iUnion, Finset.exists_coe,
exists₂_imp]
intro v hv huvt
exact hJu_subset v (h_ss hv) huvt
refine ⟨J', hJ'_subset, ?_, ?_⟩
· rw [Finset.coe_biUnion]
refine PairwiseDisjoint.biUnion ?_ ?_
· simp only [univ_eq_attach, mem_coe, id, iSup_eq_iUnion]
simp_rw [PairwiseDisjoint, Set.Pairwise]
intro x _ y _ hxy
have hxy_disj : Disjoint (x : Set α) y := by
by_contra h_contra
refine hxy ?_
refine Subtype.ext ?_
exact h_dis.elim x.prop y.prop h_contra
convert hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj
· rw [sUnion_eq_biUnion]
congr
· rw [sUnion_eq_biUnion]
congr
· exact fun u _ ↦ hJu_disj _ _
· rw [coe_insert, sUnion_insert, Set.union_comm, ← Set.diff_diff, h_eq]
simp_rw [J', sUnion_eq_biUnion, Set.iUnion_diff]
simp only [mem_coe, Finset.mem_biUnion, Finset.mem_univ, Finset.exists_coe, iUnion_exists, true_and]
rw [iUnion_comm]
refine iUnion_congr fun i ↦ ?_
by_cases hi : i ∈ J
· simp only [hi, iUnion_true]
rw [← hJu_sUnion i (h_ss hi), sUnion_eq_biUnion]
simp only [mem_coe]
· simp only [hi, iUnion_of_empty, iUnion_empty]
