hom — Mathlib

English

There is a map from components outside L to components outside K induced by inclusion K ⊆ L; i.e., a map on component complements given by restricting along the inclusion.

Русский

Существует отображение между компонентами вне L и компонентами вне K, индуцированное включением K ⊆ L.

LaTeX

$$$$ \text{hom }(h)(C) = C.map(\text{induceHom}(\mathrm{id}, \overline{h})) $$$$

Lean4

/-- If `K ⊆ L`, the components outside of `L` are all contained in a single component outside of `K`.
-/
abbrev hom (h : K ⊆ L) (C : G.ComponentCompl L) : G.ComponentCompl K :=
  C.map <| induceHom Hom.id <| Set.compl_subset_compl.2 h

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