English
The intersection of two sets s and t is the set of elements contained in both s and t: s ∩ t = {a ∈ α | a ∈ s and a ∈ t}.
Русский
Пересечение двух множеств s и t — множество элементов, принадлежащих и s, и t: s ∩ t = {a ∈ α | a ∈ s и a ∈ t}.
LaTeX
$$$s \cap t = \{x \in \alpha \mid x \in s \land x \in t\}$$$
Lean4
/-- The intersection of two sets `s` and `t` is the set of elements contained in both `s` and `t`.
Note that you should **not** use this definition directly, but instead write `s ∩ t`. -/
protected def inter (s₁ s₂ : Set α) : Set α :=
{a | a ∈ s₁ ∧ a ∈ s₂}
