end_componentCompl_infinite — Mathlib

English

The component-complements chosen by an end have infinite support for every finite subset.

Русский

Компонентные дополнения, выбираемые концом, имеют бесконечную поддержку для каждого конечного подмножества.

LaTeX

$$$\\forall e\\in G.end, \\forall K, (e:\$Finset\\ V\$^{op} \\to G.componentComplFunctor.obj K).supp.Infinite$$$

Lean4

/-- The `componentCompl`s chosen by an end are all infinite. -/
theorem end_componentCompl_infinite (e : G.end) (K : (Finset V)ᵒᵖ) :
    ((e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K).supp.Infinite :=
  by
  refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)
  change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h
  exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩

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