exists_eq_ofArrows — Mathlib

English

Every presieve on X has a representation as ofArrows data; i.e., there exists indices and arrows realizing R as ofArrows.

Русский

Каждая предсистема на X имеет представление в виде данных ofArrows; то есть существуют индексы и стрелы, реализующие R как ofArrows.

LaTeX

$$$\\exists ι\\; (Y:ι\\to C)\\; (f: \\forall i, Y_i\\to X) ,\\; R = \\mathrm{ofArrows} Y f$$$

Lean4

theorem exists_eq_ofArrows (R : Presieve X) :
    ∃ (ι : Type (max u₁ v₁)) (Y : ι → C) (f : ∀ i, Y i ⟶ X), R = .ofArrows Y f :=
  by
  let ι := { x : Σ Z, (Z ⟶ X) // R x.2 }
  use ι, fun x ↦ x.1.1, fun x ↦ x.1.2
  exact le_antisymm (fun Z g hg ↦ .mk (⟨⟨_, _⟩, hg⟩ : ι)) fun Z g ⟨x⟩ ↦ x.2

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