English
The family (lapMatrix_ker_basis_aux G) indexed by the connected components of G is linearly independent over ℝ.
Русский
Множество (lapMatrix_ker_basis_aux G), индексируемое по связным компонентам G, линейно независимо над ℝ.
LaTeX
$$$$ \\text{LinearIndependent}_{\\mathbb{R}}\\bigl( \\{ \\mathrm{lapMatrix\\_ker\\_basis\\_aux}(G)(c) \\mid c \\in G.ConnectedComponent \\} \\bigr). $$$$
Lean4
theorem edgeSet_map (f : V ↪ W) (G : SimpleGraph V) : (G.map f).edgeSet = f.sym2Map '' G.edgeSet :=
by
ext v
induction v
rw [mem_edgeSet, map_adj, Set.mem_image]
constructor
· intro ⟨a, b, hadj, ha, hb⟩
use s(a, b), hadj
rw [Embedding.sym2Map_apply, Sym2.map_pair_eq, ha, hb]
· intro ⟨e, hadj, he⟩
induction e
rw [Embedding.sym2Map_apply, Sym2.map_pair_eq, Sym2.eq_iff] at he
exact he.elim (fun ⟨h, h'⟩ ↦ ⟨_, _, hadj, h, h'⟩) (fun ⟨h', h⟩ ↦ ⟨_, _, hadj.symm, h, h'⟩)
