pullback_fst_range — Mathlib

English

The range of the fst projection from the pullback equals the set of pairs (x,y) with f(x) = g(y).

Русский

Образ fst-проекции пределa равен множеству пар (x,y) таких, что f(x) = g(y).

LaTeX

$$$ \operatorname{range}( \mathrm{pullback.fst} f g ) = \{ x : X \mid \exists y : Y, f x = g y \} $$$

Lean4

theorem pullback_fst_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :
    Set.range (pullback.fst f g) = {x : X | ∃ y : Y, f x = g y} :=
  by
  ext x
  constructor
  · rintro ⟨y, rfl⟩
    use pullback.snd f g y
    exact CategoryTheory.congr_fun pullback.condition y
  · rintro ⟨y, eq⟩
    use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
    rw [pullbackIsoProdSubtype_inv_fst_apply]

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