Homework (VI)

Problem 1

In the Lean Lab we proved that if $A \subset B$ then $\mathcal{P} (A) \subset \mathcal{P} (B)$. Can you prove the converse in Lean?

Problem 2

In the code below we define the notion of “disjoint sets”. Prove the theorem in the code by filling in sorry.