English
For locally finite G and G.preconnected, the set of components outside any finite K is finite.
Русский
Для локально конечного графа G и предподсоединённости графа множество компонент вне любого конечного K конечно.
LaTeX
$$$$ \text{Finite}(G.\operatorname{ComponentCompl} K) $$$$
Lean4
/-- For a locally finite preconnected graph, the number of components outside of any finite set
is finite. -/
instance componentCompl_finite [LocallyFinite G] [Gpc : Fact G.Preconnected] (K : Finset V) :
Finite (G.ComponentCompl K) := by
classical
rcases K.eq_empty_or_nonempty with rfl | h
· dsimp [ComponentCompl]
rw [Finset.coe_empty, Set.compl_empty]
have := Gpc.out.subsingleton_connectedComponent
exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
· let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
let p := C.exists_adj_boundary_pair Gpc.out h
⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
-- `touch` is injective
have touch_inj : touch.Injective := fun C D h' =>
ComponentCompl.pairwise_disjoint.eq
(Set.not_disjoint_iff.mpr
⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
-- `touch` has finite range
have : Finite (Set.range touch) :=
by
refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
-- hence `touch` has a finite domain
apply Finite.of_injective_finite_range touch_inj
