uncurry_ofArrows — Mathlib

English

If s is built from arrows Y_i → X, then its uncurry is exactly the range of the map i ↦ ⟨Y_i, f_i⟩.

Русский

Если presieve построен из стрел Y_i → X, то его uncurry ровно равен множеству пар, полученных образом i ↦ ⟨Y_i, f_i⟩.

LaTeX

$$$(\\mathrm{ofArrows}\\ Y\\ f).\\mathrm{uncurry} = \\mathrm{Set.range}\; (\\lambda i \\; \\mapsto \\langle Y i, f i \\rangle)$$$

Lean4

@[simp]
theorem uncurry_ofArrows {ι : Type*} (Y : ι → C) (f : (i : ι) → Y i ⟶ X) :
    (ofArrows Y f).uncurry = Set.range fun i : ι ↦ ⟨_, f i⟩ :=
  by
  ext ⟨Z, v⟩; simp only [Set.mem_range, Sigma.mk.injEq]; constructor
  · rintro ⟨i⟩; exact ⟨_, rfl, HEq.refl _⟩
  · rintro ⟨i, rfl, h⟩; rw [← eq_of_heq h]; exact ⟨i⟩

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