hom_refl — Mathlib

English

The homomorphism on a component-complement is the identity map on the components.

Русский

Гомоморфизм в компонентном дополнении равен тождественному отображению на компонентах.

LaTeX

$$$\\text{hom}$ acts as the identity on each component; in particular, $\\text{hom}(C) = C$ for every component.$$

Lean4

theorem hom_refl (C : G.ComponentCompl L) : C.hom (subset_refl L) = C :=
  by
  change C.map _ = C
  rw [induceHom_id G Lᶜ, ConnectedComponent.map_id]

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