Theorems · Theorem · combinatorics

SimpleGraph.isBipartiteWith_neighborFinset_subset

∀ {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.neighborFinset v ⊆ t

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

Defined in

Mathlib.Combinatorics.SimpleGraph.Bipartite

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fintype