diag_image — Mathlib

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]

Похожие утверждения