English
Let G be a simple graph and let c be a connected component of G. The function f: V → ℝ defined by f(i) = 1 if i belongs to c and f(i) = 0 otherwise lies in the kernel of the linear map toLin' (lapMatrix ℝ G). In other words, the indicator of a connected component is a nullspace vector.
Русский
Пусть G — простой граф, а c — связная компонента G. Функция f: V → ℝ, заданная как f(i) = 1, если i ∈ c, и иначе f(i) = 0, принадлежит ядру линейного отображения toLin'(lapMatrix ℝ G). Иными словами, индикатор компоненты лежит в нулевом подпространстве.
LaTeX
$$$$ f(i) = \\begin{cases}1, & i \\in c, \\\\ 0, & i \\notin c\\end{cases} \\quad \\text{and} \\quad f \\in \\ker\\bigl( \\text{toLin}'(G.lapMatrix \\mathbb{R}) \\bigr). $$$$
Lean4
theorem mem_ker_toLin'_lapMatrix_of_connectedComponent {G : SimpleGraph V} [DecidableRel G.Adj]
[DecidableEq G.ConnectedComponent] (c : G.ConnectedComponent) :
(fun i ↦ if connectedComponentMk G i = c then 1 else 0) ∈ LinearMap.ker (toLin' (lapMatrix ℝ G)) :=
by
rw [LinearMap.mem_ker, toLin'_apply, lapMatrix_mulVec_eq_zero_iff_forall_reachable]
intro i j h
split_ifs with h₁ h₂ h₃
· rfl
· rw [← ConnectedComponent.eq] at h
exact (h₂ (h₁ ▸ h.symm)).elim
· rw [← ConnectedComponent.eq] at h
exact (h₁ (h₃ ▸ h)).elim
· rfl
