connectedComponentEquiv_symm — Mathlib

English

The equivalence induced by φ.symm is the inverse of the equivalence induced by φ.

Русский

Эквивелентность, порожденная φ.symm, является обратной к эквивелентности, порожденной φ.

LaTeX

$$$\\\\text{connectedComponentEquiv}(\\\\phi).symm = \\\\text{connectedComponentEquiv}(\\\\phi.symm)$$$

Lean4

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

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