isBipartiteWith_degree_le — Mathlib

English

If G.IsBipartiteWith s t and v ∈ s, then deg(v) ≤ |t|.

Русский

Пусть G IsBipartiteWith s t и v ∈ s, тогда deg(v) ≤ |t|.

LaTeX

$$G.IsBipartiteWith s t → v ∈ s → G.degree v ≤ |t|$$

Lean4

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

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