English
There exists a function-like mapping K : Set α → Finset (Set α) with several disjointness properties partitioning unions.
Русский
Существует отображение K, разбивающее объединения на частичные неперекрывающиеся множества.
LaTeX
$$$$ \\exists K : Set α \\to Finset (Set α), \\; PairwiseDisjoint J K \\; \\land \\; \\forall i \\in J, \\; ↑(K i) \\subseteq C \\land \\dots $$$$
Lean4
theorem disjointOfUnion_props (hC : IsSetSemiring C) (h1 : ↑J ⊆ C) :
∃ K : Set α → Finset (Set α),
PairwiseDisjoint J K ∧
(∀ i ∈ J, ↑(K i) ⊆ C) ∧
PairwiseDisjoint (⋃ x ∈ J, (K x : Set (Set α))) id ∧
(∀ j ∈ J, ⋃₀ K j ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ J = ⋃₀ (⋃ x ∈ J, (K x : Set (Set α))) :=
by
classical
induction J using Finset.cons_induction with
| empty => simp
| cons s J hJ hind =>
rw [cons_eq_insert, coe_insert, Set.insert_subset_iff] at h1
obtain ⟨K, hK0, ⟨hK1, hK2, hK3, hK4, hK5⟩⟩ := hind h1.2
let K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then (hC.disjointOfDiffUnion h1.1 h1.2) else K t
have hK1s : K1 s = hC.disjointOfDiffUnion h1.1 h1.2 := by simp [K1]
have hK1_of_ne t (ht : t ≠ s) : K1 t = K t := by simp [K1, ht]
use K1
simp only [cons_eq_insert, mem_coe, Finset.mem_insert, sUnion_subset_iff, forall_eq_or_imp, coe_insert,
sUnion_insert]
-- two simplification rules for induction hypothesis
have ht1' : ∀ x ∈ J, K1 x = K x := fun x hx ↦ hK1_of_ne _ (fun h_eq ↦ hJ (h_eq ▸ hx))
have ht2 : (⋃ x ∈ J, (K1 x : Set (Set α))) = ⋃ x ∈ J, ((K x : Set (Set α))) :=
by
apply iUnion₂_congr
intro x hx
exact_mod_cast hK1_of_ne _ (ne_of_mem_of_not_mem hx hJ)
simp only [hK1s]
refine
⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_, ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_,
?_⟩
· apply Set.Pairwise.insert
· intro j hj i hi hij
rw [Function.onFun, ht1' j hj, ht1' i hi]
exact hK0 hj hi hij
· intro i hi _
have h7 : Disjoint ↑(hC.disjointOfDiffUnion h1.1 h1.2) (K i : Set (Set α)) :=
by
refine
disjoint_of_sSup_disjoint_of_le_of_le (hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2) ?_
(@disjoint_sdiff_left _ (⋃₀ J) s) (Or.inl (hC.empty_notMem_disjointOfDiffUnion h1.1 h1.2))
simp only [mem_coe, Set.le_eq_subset]
apply sUnion_subset_iff.mp
exact (hK3 i hi).trans (subset_sUnion_of_mem hi)
have h8 : Function.onFun Disjoint K1 s i :=
by
refine Finset.disjoint_iff_inter_eq_empty.mpr ?_
rw [ht1' i hi, hK1s]
rw [Set.disjoint_iff_inter_eq_empty] at h7
exact_mod_cast h7
exact ⟨h8, Disjoint.symm h8⟩
· intro i hi
rw [ht1' i hi]
exact hK1 i hi
· simp only [iUnion_iUnion_eq_or_left]
refine pairwiseDisjoint_union.mpr ⟨?_, ?_, ?_⟩
· rw [hK1s]
exact hC.pairwiseDisjoint_disjointOfDiffUnion h1.1 h1.2
· simpa [ht2]
· simp only [mem_coe, mem_iUnion, exists_prop, ne_eq, id_eq, forall_exists_index, and_imp]
intro i hi j x hx h3 h4
obtain ki : i ⊆ s \ ⋃₀ J := hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2 _ (hK1s ▸ hi)
obtain hx2 : j ⊆ x := subset_trans (subset_sUnion_of_mem (ht1' x hx ▸ h3)) (hK3 x hx)
obtain kj : j ⊆ ⋃₀ J := hx2.trans <| subset_sUnion_of_mem hx
exact disjoint_of_subset ki kj disjoint_sdiff_left
· intro a ha
simp_rw [hK1_of_ne _ (ne_of_mem_of_not_mem ha hJ)]
change ∀ t' ∈ (K a : Set (Set α)), t' ⊆ a
rw [← sUnion_subset_iff]
exact hK3 a ha
· refine ⟨hC.empty_notMem_disjointOfDiffUnion h1.1 h1.2, ?_⟩
intro a ha
rw [ht1' a ha]
exact hK4 a ha
· simp only [iUnion_iUnion_eq_or_left, sUnion_union, ht2, K1]
simp_rw [apply_ite, hK5, ← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion h1.1 h1.2, hK5]
simp only [↓reduceIte, diff_union_self]
