English
Let G be a simple graph on V and s an end of G. For finite L and K with L ⊆ K, and a vertex v ∉ L, if the value s assigns to L equals the component-complement at v, then the value of s on K is the component-complement at the image of v under the inclusion L ⊆ K.
Русский
Пусть G — простой граф на \(V\) и \(s\) — конец графа. Для конечных множеств \(L\) и \(K\) с \(L \subseteq K\), и вершины \(v\notin L\), если значение \(s\) на \(L\) равно компонентному дополнению в вершине \(v\), то значение \(s\) на \(K\) равно компонентному дополнению в вершине, получившейся из \(v\) под вложением \(L \subseteq K\).
LaTeX
$$$\\forall s \\in G.end, \\forall L, K \\subseteq V\\text{ конечны}, \\forall h:\\ L \\hookrightarrow K, \\forall v:\\ V, v \\notin L, s(L) = G.componentComplMk(v) \\Rightarrow s(K) = G.componentComplMk(v_K) \\;,$$$
Lean4
theorem end_hom_mk_of_mk {s} (sec : s ∈ G.end) {K L : (Finset V)ᵒᵖ} (h : L ⟶ K) {v : V} (vnL : v ∉ L.unop)
(hs : s L = G.componentComplMk vnL) : s K = G.componentComplMk (Set.notMem_subset (le_of_op_hom h : _ ⊆ _) vnL) :=
by
rw [← sec h, hs]
apply ComponentCompl.hom_mk _ (le_of_op_hom h : _ ⊆ _)
