isBipartiteWith_degree_le' — Mathlib

English

If G is bipartite with parts s and t and w ∈ t, then the degree of w in G is at most the size of s.

Русский

Если граф G двудольный с частями s и t и вершина w принадлежит t, то степень вершины w в G не больше размера множества s.

LaTeX

$$$G.IsBipartiteWith(s,t) \land w \in t \Rightarrow G.degree(w) \le |s|$$$

Lean4

/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the degree of `w` in `G` is at most the size of
`s`. -/
theorem isBipartiteWith_degree_le' (h : G.IsBipartiteWith s t) (hw : w ∈ t) : G.degree w ≤ #s :=
  by
  rw [← card_neighborFinset_eq_degree]
  exact card_le_card (isBipartiteWith_neighborFinset_subset' h hw)

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