mono — Mathlib

English

If G'' is a subgraph of G and G is alternating with respect to G', then G'' is alternating with respect to G'.

Русский

Если G'' является подграфом G и G чередуется относительно G', то G'' также чередуется относительно G'.

LaTeX

$$$ (G'' \le G) \wedge (G.IsAlternating G') \Rightarrow (G'' IsAlternating G') $$$

Lean4

theorem mono {G'' : SimpleGraph V} (halt : G.IsAlternating G') (h : G'' ≤ G) : G''.IsAlternating G' :=
  fun _ _ _ hww' hvw hvw' ↦ halt hww' (h hvw) (h hvw')

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