def Finpartition.multipartiteGraph {α : Type u_1} [Fintype α] [DecidableEq α] (P : Finpartition Finset.univ) : SimpleGraph α

Equations

• P.multipartiteGraph = { Adj := fun (a b : α) => ∀ ⦃s : Finset α⦄, s ∈ P.parts → a ∈ s → b ∉ s, symm := ⋯, loopless := ⋯ }

@[simp]

theorem Finpartition.multipartiteGraph_adj {α : Type u_1} [Fintype α] [DecidableEq α] (P : Finpartition Finset.univ) (a b : α) : P.multipartiteGraph.Adj a b = ∀ ⦃s : Finset α⦄, s ∈ P.parts → a ∈ s → b ∉ s

instance Finpartition.instDecidableRelAdjMultipartiteGraph {α : Type u_1} [Fintype α] [DecidableEq α] {P : Finpartition Finset.univ} : DecidableRel P.multipartiteGraph.Adj

Equations

• Finpartition.instDecidableRelAdjMultipartiteGraph x✝ x = Finset.decidableDforallFinset

theorem Finpartition.multipartiteGraph_adj_of_mem_parts {α : Type u_1} [Fintype α] [DecidableEq α] {P : Finpartition Finset.univ} {s t : Finset α} {a b : α} (hs : s ∈ P.parts) (ht : t ∈ P.parts) (ha : a ∈ s) (hb : b ∈ t) : P.multipartiteGraph.Adj a b ↔ s ≠ t

If v and w are in distinct parts then they are adjacent.