preimage_coe_coe_diagonal — Mathlib

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]

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