ofHoms_iff — Mathlib

English

Let f_i be a family of arrows X_i ⟶ Y_i indexed by i ∈ ι, and g: A ⟶ B. Then the property of transporting along the family holds exactly when there exists i with Arrow.mk g = Arrow.mk (f_i).

Русский

Пусть дано семейство стрелок f_i: X_i ⟶ Y_i, индексируемое i ∈ ι, и г: A ⟶ B. Тогда свойство переносится ровно тогда, когда существует i, такое что Arrow.mk g = Arrow.mk (f_i).

LaTeX

$$$\mathrm{ofHoms} f g \iff \exists i, \mathrm{Arrow.mk} g = \mathrm{Arrow.mk}(f i)$$$

Lean4

theorem ofHoms_iff {ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) {A B : C} (g : A ⟶ B) :
    ofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i) := by
  constructor
  · rintro ⟨i⟩
    exact ⟨i, rfl⟩
  · rintro ⟨i, h⟩
    rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]
    constructor

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