English
The image of s under the diagonal map equals the intersection of the diagonal with s × s.
Русский
Образ через диагональное отображение равен пересечению диагонали с s × s.
LaTeX
$$$(\\lambda x. (x,x))\\,''\\,s = \\Delta(\\alpha) \\cap (s \\times s)$$$
Lean4
theorem diag_image (s : Set α) : (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s := by
rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]