English
For a finite K ⊆ V and a component C outside K, C.supp is infinite if and only if for every L ⊇ K there exists D ∈ G.ComponentCompl L with D.hom h = C.
Русский
Для конечного K и компоненты C вне K множество ограничений бесконечно тогда и только тогда, когда для каждого L ⊇ K существует D ∈ G.ComponentCompl L с D.hom h = C.
LaTeX
$$$$ C.supp.Infinite \iff \forall L (h: K \subseteq L), \exists D:\ G.ComponentCompl L, D.hom h = C $$$$
Lean4
theorem infinite_iff_in_all_ranges {K : Finset V} (C : G.ComponentCompl K) :
C.supp.Infinite ↔ ∀ (L) (h : K ⊆ L), ∃ D : G.ComponentCompl L, D.hom h = C := by
classical
constructor
· rintro Cinf L h
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
exact ⟨componentComplMk _ vL, rfl⟩
· rintro h Cfin
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left
obtain ⟨v, vD⟩ := D.nonempty
let Ddis := D.disjoint_right
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left, Set.disjoint_iff] at Ddis
exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩
