2020-02-21 13:15:42 +0100 | asked a question | How to solve logic proofs -- 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 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 |