-- Instructions: Replace all "sorry"s with proofs.
-- Hint: The two lemmas are lemmas and not examples for a reason.
open set
variables {U I : Type}
variables A B C : set U
variables D E : I → set U
variable u : U
def Union (A : I → set U) : set U := { x | ∃ i : I, x ∈ A i }
notation ∪ binders , r:(scoped f, Union f) := r
def Inter (A : I → set U) : set U := { x | ∀ i : I, x ∈ A i }
notation ∩ binders , r:(scoped f, Inter f) := r
variable ext {A B : set U} (h : ∀ x : U, x ∈ A ↔ x ∈ B) : A = B
1.example : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := sorry
2.example : (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) := sorry
3.lemma subsets_are_transitive {X Y Z : set U} (h1 : X ⊆ Y) (h2 : Y ⊆ Z) : X ⊆ Z := sorry
4.lemma biggest_subset (X : set U) : X ∈ powerset X := sorry
5.example : (A ⊆ B) ↔ (powerset A) ⊆ (powerset B) := sorry
