Theorems · Theorem · combinatorics

SimpleGraph.isBipartiteWith_neighborFinset_disjoint

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

If G.IsBipartiteWith s t and v ∈ s, then the neighbor finset of v is disjoint to s.

Defined in

Mathlib.Combinatorics.SimpleGraph.Bipartite

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fintype