Theorems · Theorem · combinatorics

SimpleGraph.isBipartiteWith_neighborFinset

∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)]
  [inst_1 : DecidableRel G.Adj], G.IsBipartiteWith ↑s ↑t → v ∈ s → G.neighborFinset v = {w ∈ t | G.Adj v w}

If G.IsBipartiteWith s t and v ∈ s, then the neighbor finset of v is the set of vertices in s adjacent to v in G.

Defined in

Mathlib.Combinatorics.SimpleGraph.Bipartite

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRel