Slate - Intersection with empty left argument is empty

Proposition 1.1.15. Let S be a set. Then:

∅ ∩ S = ∅

Proof.

By 1.1.12.
By 1.1.2.

References.

https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.empty_inter