iso_inv_image_comp_eq_iff_eq_map — Mathlib

English

If the connected component of φ.symm(v') in G equals a component C, then the component of v' in G' equals the image C.map φ.

Русский

Если компонента связности в G, содержащая φ.symm(v'), равна компоненте C, тогда компонента связности в G' для v' равна образу C под φ.

LaTeX

$$$G.connectedComponentMk (\\\\phi. symm v') = C \\\\iff \\\\ G'.connectedComponentMk v' = C.map \\\\phi$$$

Lean4

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

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