connectedComponentEquiv_trans — Mathlib

English

The composition of isomorphisms corresponds to the composition of their induced component equivalences.

Русский

Состязание изоморфизмов соответствует композиции их индуцированных эквивалентностей компонент.

LaTeX

$$$\\\\text{connectedComponentEquiv}(\\\\phi \\\\circ \\\\psi) = \\\\text{connectedComponentEquiv}(\\\\phi) \\\\circ \\\\text{connectedComponentEquiv}(\\\\psi)$$$

Lean4

@[simp]
theorem connectedComponentEquiv_trans (φ : G ≃g G') (φ' : G' ≃g G'') :
    connectedComponentEquiv (φ.trans φ') = φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv :=
  by
  ext ⟨_⟩
  rfl

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