iso_image_comp_eq_map_iff_eq_comp

English

For an isomorphism φ: G ≃g G', the induced map yields a bijection between the connected components of G and those of G'.

Русский

Для изоморфизма φ: G ≃g G' полученная карта задаёт биективное соответствие между компонентами связности G и G'.

LaTeX

$$$\\\\forall {C : G.ConnectedComponent},\\\\exists D : G'.ConnectedComponent, D = (G'.connectedComponentMk (\\\\phi v))$$$

Lean4

@[simp]
theorem iso_image_comp_eq_map_iff_eq_comp {C : G.ConnectedComponent} :
    G'.connectedComponentMk (φ v) = C.map ↑(↑φ : G ↪g G') ↔ G.connectedComponentMk v = C :=
  by
  refine C.ind fun u => ?_
  simp only [Iso.reachable_iff, ConnectedComponent.map_mk, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding,
    ConnectedComponent.eq]

Похожие утверждения