From a72f6666e80097a53f2740979df8525eeca12129 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Tue, 16 Feb 2016 08:00:47 -0500 Subject: [PATCH] feat(library/data/set/basic): add two theorems --- library/data/set/basic.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 09568ad42..951dd6046 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -883,6 +883,30 @@ by rewrite [-comp_comp, comp_Union] theorem Inter_eq_comp_Union_comp {X I : Type} (s : I → set X) : (⋂ i, s i) = - (⋃ i, -s i) := by rewrite [-comp_comp, comp_Inter] +lemma inter_distrib_Union_left {X I : Type} (s : I → set X) (a : set X) : + a ∩ (⋃ i, s i) = ⋃ i, a ∩ s i := +ext (take x, iff.intro + (assume H, obtain i Hi, from and.elim_right H, + have x ∈ a ∩ s i, from and.intro (and.elim_left H) Hi, + show _, from exists.intro i this) + (assume H, obtain i [xa xsi], from H, + show _, from and.intro xa (exists.intro i xsi))) + +section + open classical + + lemma union_distrib_Inter_left {X I : Type} (s : I → set X) (a : set X) : + a ∪ (⋂ i, s i) = ⋂ i, a ∪ s i := + ext (take x, iff.intro + (assume H, or.elim H + (assume H1, take i, or.inl H1) + (assume H1, take i, or.inr (H1 i))) + (assume H, + by_cases + (suppose x ∈ a, or.inl this) + (suppose x ∉ a, or.inr (take i, or.resolve_left (H i) this)))) +end + -- these are useful for turning binary union / intersection into countable ones definition bin_ext (s t : set X) (n : ℕ) : set X :=