ranges_directed — Mathlib

English

For a cofiltred category, a functor F: C ⥤ Type*, the collection of sets { range (F.map f.2) } is directed under inclusion by ⊇.

Русский

Для кофильтрованной категории и функторa F: C ⥤ Type*, множество { range (F.map f.2) } направлено по включению относительно ⊇.

LaTeX

$$$$ \\text{Directed}(\\supseteq)\\;\\big\\{ \\mathrm{range}(F.map f.2) \\mid f \\text{ in } \\Sigma i\\, i \\to j \\big\\}. $$$$

Lean4

theorem _root_.CategoryTheory.Functor.ranges_directed (F : C ⥤ Type*) (j : C) :
    Directed (· ⊇ ·) fun f : Σ' i, i ⟶ j => Set.range (F.map f.2) := fun ⟨i, ij⟩ ⟨k, kj⟩ =>
  by
  let ⟨l, li, lk, e⟩ := cospan ij kj
  refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩ <;> simp_rw [F.map_comp] <;> apply Set.range_comp_subset_range

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