image_toPullbackDiag — Mathlib

English

The image of s under toPullbackDiag f equals the intersection of pullbackDiagonal f with (Subtype.val)^{-1}(s) × s.

Русский

Образ через toPullbackDiag f множества s равен пересечению диагонали pullback f и (Subtype.val)^{-1}(s) × s.

LaTeX

$$$toPullbackDiag(f) '' s = \\mathrm{pullbackDiagonal}(f) \\cap (\\mathrm{Subtype.val})^{-1}'(s) \\times s$$$

Lean4

theorem image_toPullbackDiag (f : X → Y) (s : Set X) :
    toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s :=
  by
  ext x
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨rfl, hx, hx⟩
  · obtain ⟨⟨x, y⟩, h⟩ := x
    rintro ⟨rfl : x = y, h2x⟩
    exact mem_image_of_mem _ h2x.1

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