ofArrows_mem_comap_jointlySurjectivePrecoverage_iff

English

If pullbacks work well for arrows, then isStableUnderBaseChange holds for presieves of arrows.

Русский

Если базовые изменения работают для стрелок, то устойчивость при базовом изменении сохраняется для пресивов стрелок.

LaTeX

$$isStableUnderBaseChange_comap_jointlySurjectivePrecoverage$$

Lean4

theorem ofArrows_mem_comap_jointlySurjectivePrecoverage_iff {X : C} {ι : Type*} {Y : ι → C} {f : ∀ i, Y i ⟶ X} :
    ofArrows Y f ∈ Types.jointlySurjectivePrecoverage.comap F X ↔
      ∀ x : F.obj X, ∃ (i : ι), x ∈ Set.range (F.map (f i)) :=
  by simp

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