spanningCoe — Mathlib

English

If G is alternating with respect to G', then for any Subgraph H of G, the spanningCoe of H is alternating with G'.

Русский

Если G чередуется относительно G', то для любого подграфа H графа G отображение spanningCoe удовлетворяет свойству чередования относительно G'.

LaTeX

$$$ (G.IsAlternating G') \to \forall H : G.Subgraph, H.spanningCoe.IsAlternating G' $$$

Lean4

theorem spanningCoe (halt : G.IsAlternating G') (H : Subgraph G) : H.spanningCoe.IsAlternating G' :=
  by
  intro v w w' hww' hvw hvv'
  simp only [Subgraph.spanningCoe_adj] at hvw hvv'
  exact halt hww' hvw.adj_sub hvv'.adj_sub

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