degree_le' — Mathlib

English

If G' ≤ G'' then deg_{G'}(v) ≤ deg_{G''}(v) for all v.

Русский

Если G' ⊆ G'', то deg_{G'}(v) ≤ deg_{G''}(v) для всех v.

LaTeX

$$$(G',G'') : Subgraph(G)\to Subgraph(G) \Rightarrow (h): G' \le G'' \to \forall v, G'.degree v \le G''.degree v$$$

Lean4

theorem degree_le' (G' G'' : Subgraph G) (h : G' ≤ G'') (v : V) [Fintype (G'.neighborSet v)]
    [Fintype (G''.neighborSet v)] : G'.degree v ≤ G''.degree v :=
  Set.card_le_card (neighborSet_subset_of_subgraph h v)

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