English
An element a belongs to s ∩ t exactly when a belongs to both s and t: a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t.
Русский
Элемент a принадлежит s ∩ t тогда и только тогда, когда a принадлежит и s, и t.
LaTeX
$$$a \\in s \\cap t \\iff a \\in s \\land a \\in t.$$$
Lean4
@[simp]
theorem mem_inter : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t :=
⟨fun h => ⟨mem_of_le inter_le_left h, mem_of_le inter_le_right h⟩, fun ⟨h₁, h₂⟩ => by
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self⟩