English
If Es i are pairwise disjoint and their union is univ, then the complement of the union over I equals the union over Iᶜ of Es i.
Русский
Если множества Es i попарно непересекаются и их объединение есть все множество, то комплемент объединения по I равен объединению по Iᶜ множества Es i.
LaTeX
$$$$\\left(\\bigcup_{i}\\, Es_i\\right)^c = \\bigcup_{i \\in I^c} Es_i,$$ при условии Es_i взаимно непересекаются и их объединение равно univ.$$
Lean4
theorem biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ {ι : Type*} {Es : ι → Set α}
(Es_union : ⋃ i, Es i = univ) (Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)) (I : Set ι) :
(⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i := by
ext x
obtain ⟨i, hix⟩ : ∃ i, x ∈ Es i := by simp [← mem_iUnion, Es_union]
have obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J :=
by
refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩
intro x_in_U
simp only [mem_iUnion, exists_prop] at x_in_U
obtain ⟨j, j_in_J, hjx⟩ := x_in_U
rwa [show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl]
have obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J := fun J ↦ by
simpa only [mem_compl_iff, not_iff_not] using obs J
rw [obs, obs', mem_compl_iff]
