Theorems · Inductive type · combinatorics

SimpleGraph.IsBipartiteWith

{V : Type u_1} → SimpleGraph V → Set V → Set V → Prop

G is bipartite in sets s and t iff s and t are disjoint and if vertices v and w are adjacent in G then v ∈ s and w ∈ t, or v ∈ t and w ∈ s.

Defined in

Mathlib.Combinatorics.SimpleGraph.Bipartite

Cited by

42 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms