Theorems · Theorem · combinatorics

SimpleGraph.isBipartiteWith_degree_le

∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)],
  G.IsBipartiteWith ↑s ↑t → v ∈ s → G.degree v ≤ t.card

If G.IsBipartiteWith s t and v ∈ s, then the degree of v in G is at most the size of t.

Defined in

Mathlib.Combinatorics.SimpleGraph.Bipartite

Cited by

0 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype