English
An isomorphism φ between graphs G and G' determines a bijection between their connected components, i.e., a canonical equivalence φ.connectedComponentEquiv: G.ConnectedComponent ≃ G'.ConnectedComponent.
Русский
Изоморфизм φ между графами G и G' определяет биекцию между их компонентами связности, т.е. каноническое эквивалентное отображение φ.connectedComponentEquiv: G.ConnectedComponent ≃ G'.ConnectedComponent.
LaTeX
$$$\\\\text{connectedComponentEquiv}(\\\\phi) : G.ConnectedComponent \\\\simeq G'.ConnectedComponent$$$
Lean4
/-- An isomorphism of graphs induces a bijection of connected components. -/
@[simps]
def connectedComponentEquiv (φ : G ≃g G') : G.ConnectedComponent ≃ G'.ConnectedComponent
where
toFun := ConnectedComponent.map φ
invFun := ConnectedComponent.map φ.symm
left_inv C := C.ind (fun v => congr_arg G.connectedComponentMk (Equiv.left_inv φ.toEquiv v))
right_inv C := C.ind (fun v => congr_arg G'.connectedComponentMk (Equiv.right_inv φ.toEquiv v))
