English
For any fixed finite subset K, and any object C in the component-complement functor at K, the support of C is infinite precisely when C lies in the eventual range of the functor at K.
Русский
Для фиксированного конечного подмножества \(K\) и любого объекта \(C\) в компонентного дополнения-функтор на \(K\), поддержка \(C\) бесконечна тогда и только тогда, когда \(C\) принадлежит эвентуальному диапазону функтору на \(K\).
LaTeX
$$$\\operatorname{Supp}(C)\\text{ Infinite} \\iff C \\in G.componentComplFunctor.eventualRange(K)$$$
Lean4
theorem infinite_iff_in_eventualRange {K : (Finset V)ᵒᵖ} (C : G.componentComplFunctor.obj K) :
C.supp.Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K :=
by
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter, Set.mem_range,
componentComplFunctor_map]
exact ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL => h (Opposite.op L) (opHomOfLE KL)⟩
