componentComplMk_mem_hom — Mathlib

English

Let G be a SimpleGraph on V, and take v ∉ K with L ⊆ K. Then v lies in the image of the homomorphism from G.componentComplMk vK via h.

Русский

Пусть G — простой граф на V, и возьмем v не из K с L ⊆ K. Тогда вершина v принадлежит образу отображения-hom из G.componentComplMk vK через h.

LaTeX

$$$ v \\in (G.componentComplMk vK).hom h $$$

Lean4

theorem _root_.SimpleGraph.componentComplMk_mem_hom (G : SimpleGraph V) {v : V} (vK : v ∉ K) (h : L ⊆ K) :
    v ∈ (G.componentComplMk vK).hom h :=
  subset_hom (G.componentComplMk vK) h (G.componentComplMk_mem vK)

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