Definition 1.1.8. Let *U* be a set, *S*, *T* ⊆ *U*. We define:

Remarks.

Due to the type system of HLM, it is impossible to define the intersection of two arbitrary sets. Instead, both sets must be declared as subsets of a common superset `U`

, although the intersection is, of course, independent of `U`

. Since a suitable value for `U`

can always be inferred automatically, `U`

can be omitted from the notation.

References.

- https://en.wikipedia.org/wiki/Intersection_(set_theory)
- https://mathworld.wolfram.com/Intersection.html
- https://proofwiki.org/wiki/Definition:Set_Intersection
- https://ncatlab.org/nlab/show/intersection
- http://metamath.tirix.org/df-in.html
- http://metamath.tirix.org/dfin5.html
- https://leanprover-community.github.io/mathlib_docs/init/data/set.html#set.inter