English
For a subset s ⊆ α, the preimage of the diagonal Δ(α) under the map Prod.map (incl_s) (incl_s) equals the diagonal Δ(s).
Русский
Для подмножества s ⊆ α предобраз диагонали через отображение включения сведёт диагональю в s.
LaTeX
$$$(\\operatorname{incl}_s^\\alpha \\times \\operatorname{incl}_s^\\alpha)^{-1}(\\Delta_\\alpha)=\\Delta_s$$$
Lean4
theorem preimage_coe_coe_diagonal (s : Set α) :
Prod.map (fun x : s => (x : α)) (fun x : s => (x : α)) ⁻¹' diagonal α = diagonal s :=
by
ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
simp [Set.diagonal]