structure Graph.Bipartition {α : Type u_1} {β : Type u_2} (G : Graph α β) : Type u_1

A bipartion of G is a partition of the vertex set into two parts such that every edge crosses the partition.

• left : Set α
• right : Set α
• union_eq : self.left ∪ self.right = G.vertexSet
• disjoint : Disjoint self.left self.right
• forall_edge (e : β) : e ∈ G.edgeSet → ∃ x ∈ self.left, ∃ y ∈ self.right, G.IsLink e x y

def Graph.Bipartition.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) : G.Bipartition

Equations

• B.symm = { left := B.right, right := B.left, union_eq := ⋯, disjoint := ⋯, forall_edge := ⋯ }

@[simp]

theorem Graph.Bipartition.symm_right {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) : B.symm.right = B.left

@[simp]

theorem Graph.Bipartition.symm_left {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) : B.symm.left = B.right

theorem Graph.Bipartition.left_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) : B.left ⊆ G.vertexSet

theorem Graph.Bipartition.right_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) : B.right ⊆ G.vertexSet

theorem Graph.Bipartition.notMem_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {B : G.Bipartition} (hx : x ∈ B.left) : x ∉ B.right

theorem Graph.Bipartition.notMem_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {B : G.Bipartition} (hx : x ∈ B.right) : x ∉ B.left

theorem Graph.Bipartition.notMem_right_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {B : G.Bipartition} (hxV : x ∈ G.vertexSet) : x ∉ B.right ↔ x ∈ B.left

theorem Graph.Bipartition.notMem_left_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {B : G.Bipartition} (hxV : x ∈ G.vertexSet) : x ∉ B.left ↔ x ∈ B.right

structure Graph.Bipartition.Same {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) (x y : α) : Prop

B.Same x y means that x and y are on the same side of B. If G is connected, this is equivalent to x and y having even distance; see Bipartiton.same_iff_dist_even.

• left_mem : x ∈ G.vertexSet
• right_mem : y ∈ G.vertexSet
• mem_left_iff : x ∈ B.left ↔ y ∈ B.left

theorem Graph.Bipartition.same_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) (x y : α) : B.Same x y ↔ x ∈ G.vertexSet ∧ y ∈ G.vertexSet ∧ (x ∈ B.left ↔ y ∈ B.left)

theorem Graph.Bipartition.Same.mem_right_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (h : B.Same x y) : x ∈ B.right ↔ y ∈ B.right

theorem Graph.Bipartition.Same.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (h : B.Same x y) : B.Same y x

theorem Graph.Bipartition.same_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} : B.Same x y ↔ B.Same y x

@[simp]

theorem Graph.Bipartition.same_self_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {B : G.Bipartition} : B.Same x x ↔ x ∈ G.vertexSet

@[simp]

theorem Graph.Bipartition.symm_same {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : G.Bipartition} : B.symm.Same = B.Same

structure Graph.Bipartition.Opp {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) (x y : α) : Prop

B.Opp x y means that x and y are on opposite sides of B. If G is connected, this is equivalent to x and y having odd distance; see Bipartiton.opp_iff_dist_odd.

• left_mem : x ∈ G.vertexSet
• right_mem : y ∈ G.vertexSet
• mem_left_iff : x ∈ B.left ↔ y ∈ B.right

theorem Graph.Bipartition.opp_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) (x y : α) : B.Opp x y ↔ x ∈ G.vertexSet ∧ y ∈ G.vertexSet ∧ (x ∈ B.left ↔ y ∈ B.right)

theorem Graph.Bipartition.Opp.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (h : B.Opp x y) : B.Opp y x

theorem Graph.Bipartition.opp_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} : B.Opp x y ↔ B.Opp y x

theorem Graph.Bipartition.Opp.mem_right_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (h : B.Opp x y) : x ∈ B.right ↔ y ∈ B.left

theorem Graph.Bipartition.not_opp_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : ¬B.Opp x y ↔ B.Same x y

theorem Graph.Bipartition.not_same_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : ¬B.Same x y ↔ B.Opp x y

theorem Graph.Bipartition.Same.not_opp {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (hB : B.Same x y) : ¬B.Opp x y

theorem Graph.Bipartition.Opp.not_same {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : G.Bipartition} (hB : B.Opp x y) : ¬B.Same x y

theorem Graph.Bipartition.opp_of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (B : G.Bipartition) (hxy : G.Adj x y) : B.Opp x y

theorem Graph.Bipartition.mem_right_of_mem_left_of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (B : G.Bipartition) (hx : x ∈ B.left) (hxy : G.Adj x y) : y ∈ B.right

theorem Graph.Bipartition.mem_left_of_mem_right_of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (B : G.Bipartition) (hx : x ∈ B.right) (hxy : G.Adj x y) : y ∈ B.left

theorem Graph.Bipartition.neighbor_subset_right_of_mem_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (B : G.Bipartition) (hx : x ∈ B.left) : N(G, x) ⊆ B.right

theorem Graph.Bipartition.neighbor_subset_left_of_mem_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (B : G.Bipartition) (hx : x ∈ B.right) : N(G, x) ⊆ B.left

theorem Graph.Bipartition.setNeighbor_subset_right_of_subset_left {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) {S : Set α} (hS : S ⊆ B.left) : N(G, S) ⊆ B.right

theorem Graph.Bipartition.setNeighbor_subset_left_of_subset_right {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) {S : Set α} (hS : S ⊆ B.right) : N(G, S) ⊆ B.left

@[simp]

theorem Graph.Bipartition.symm_opp {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : G.Bipartition} : B.symm.Opp = B.Opp

theorem Graph.Bipartition.Opp.trans {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y z : α} {B : G.Bipartition} (hxy : B.Opp x y) (hyz : B.Opp y z) : B.Same x z

theorem Graph.Bipartition.Same.trans {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y z : α} {B : G.Bipartition} (hxy : B.Same x y) (hyz : B.Same y z) : B.Same x z

@[simp]

theorem Graph.not_opp_self {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) (x : α) : ¬B.Opp x x

def Graph.Bipartition.of_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (B : H.Bipartition) (hHG : H ≤s G) (h_isLink : ∀ ⦃x y : α⦄ ⦃e : β⦄, e ∉ H.edgeSet → G.IsLink e x y → B.Opp x y) : G.Bipartition

Equations

• B.of_isSpanningSubgraph hHG h_isLink = { left := B.left, right := B.right, union_eq := ⋯, disjoint := ⋯, forall_edge := ⋯ }

def Graph.Bipartition.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (B : G.Bipartition) (hle : H ≤ G) : H.Bipartition

Equations

• B.of_le hle = { left := B.left ∩ H.vertexSet, right := B.right ∩ H.vertexSet, union_eq := ⋯, disjoint := ⋯, forall_edge := ⋯ }

def Graph.Bipartition.iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {H : ι → Graph α β} (B : (i : ι) → (H i).Bipartition) (hdj : Pairwise (Function.onFun StronglyDisjoint H)) : (Graph.iUnion H ⋯).Bipartition

Equations

• Graph.Bipartition.iUnion B hdj = { left := ⋃ (i : ι), (B i).left, right := ⋃ (i : ι), (B i).right, union_eq := ⋯, disjoint := ⋯, forall_edge := ⋯ }

def Graph.Bipartition.sUnion {α : Type u_1} {β : Type u_2} {s : Set (Graph α β)} (B : (G : Graph α β) → G ∈ s → G.Bipartition) (hs : s.Pairwise StronglyDisjoint) : (Graph.sUnion s ⋯).Bipartition

Equations

• Graph.Bipartition.sUnion B hs = { left := ⋃ (G : ↑s), (B ↑G ⋯).left, right := ⋃ (G : ↑s), (B ↑G ⋯).right, union_eq := ⋯, disjoint := ⋯, forall_edge := ⋯ }

noncomputable def Graph.Bipartition.union {α : Type u_1} {β : Type u_2} (G H : Graph α β) (B₁ : G.Bipartition) (B₂ : H.Bipartition) (hGH : G.StronglyDisjoint H) : (G ∪ H).Bipartition

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Graph.Bipartition.symm_on {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) (x : α) (_hx : x ∈ G.vertexSet) : G.Bipartition

Rather than switching the entire bipartition, we can switch the bipartition for the component containing x.

Equations

• One or more equations did not get rendered due to their size.

def Graph.Bipartite {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

A graph with a bipartition is bipartite.

Equations

• G.Bipartite = Nonempty G.Bipartition

theorem Graph.Bipartition.bipartite {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) : G.Bipartite

theorem Graph.Bipartite.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Bipartite) (hle : H ≤ G) : H.Bipartite

A subgraph of a bipartite graph is bipartite

theorem Graph.Bipartite.loopless {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Bipartite) : G.Loopless

theorem Graph.iUnion_stronglyDisjoint_bipartite {α : Type u_1} {β : Type u_2} {ι : Type u_3} {H : ι → Graph α β} (hdj : Pairwise (Function.onFun StronglyDisjoint H)) (hbp : ∀ (i : ι), (H i).Bipartite) : (Graph.iUnion H ⋯).Bipartite

A disjoint union of bipartite graphs is bipartite.

theorem Graph.sUnion_stronglyDisjoint_bipartite {α : Type u_1} {β : Type u_2} {s : Set (Graph α β)} (hdj : s.Pairwise StronglyDisjoint) (hbp : ∀ G ∈ s, G.Bipartite) : (Graph.sUnion s ⋯).Bipartite

theorem Graph.union_stronglyDisjoint_bipartite {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Bipartite) (hH : H.Bipartite) (hGH : G.StronglyDisjoint H) : (G ∪ H).Bipartite

theorem Graph.bipartite_iff_forall_component {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Bipartite ↔ ∀ (H : Graph α β), H.IsCompOf G → H.Bipartite

theorem Graph.Bipartition.same_first_get_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (B : G.Bipartition) {W : WList α β} (hW : G.IsWalk W) {n : ℕ} (hn : n ≤ W.length) : B.Same W.first (W.get n) ↔ Even n

theorem Graph.Bipartition.opp_first_get_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} {n : ℕ} (B : G.Bipartition) (hW : G.IsWalk W) (hn : n ≤ W.length) : B.Opp W.first (W.get n) ↔ Odd n

theorem Graph.Bipartition.vertex_isChain_opp {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (B : G.Bipartition) (hW : G.IsWalk W) : List.IsChain (fun (x1 x2 : α) => B.Opp x1 x2) W.vertex

theorem Graph.Bipartition.same_iff_even_dist {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (B : G.Bipartition) (hG : G.Connected) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : B.Same x y ↔ Even (G.dist x y)

theorem Graph.Bipartition.opp_iff_odd_dist {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (B : G.Bipartition) (hG : G.Connected) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : B.Opp x y ↔ Odd (G.dist x y)

theorem Graph.Bipartite.length_even_of_isWalk_isClosed {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hG : G.Bipartite) (hC : G.IsWalk C) (h_closed : C.IsClosed) : Even C.length

Every closed walk in a bipartite graph has an even number of edges.

theorem Graph.bipartite_of_forall_parity_adj_swap {α : Type u_1} {β : Type u_2} {G : Graph α β} {r : α} (h : ∀ ⦃x y : α⦄, G.Adj x y → (Odd (G.dist r x) ↔ Even (G.dist r y))) : G.Bipartite

If there is vertex r such that adjacent vertices always have opposite-parity distance to r, then G is bipartite.

theorem Graph.IsForest.bipartite {α : Type u_1} {β : Type u_2} {F : Graph α β} (hF : F.IsForest) : F.Bipartite

theorem Graph.bipartite_iff_forall_cycle_even {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Bipartite ↔ ∀ (C : WList α β), G.IsCyclicWalk C → Even C.length

A graph is bipartite if and only if all its cycles are even

def Graph.CompleteBipartiteGraph.bipartition (m n : ℕ) : (CompleteBipartiteGraph m n).Bipartition

The obvious bipartition of a complete bipartite graph.

Equations

• Graph.CompleteBipartiteGraph.bipartition m n = { left := Sum.inl '' Set.Iio m, right := Sum.inr '' Set.Iio n, union_eq := ⋯, disjoint := ⋯, forall_edge := ⋯ }

@[simp]

theorem Graph.CompleteBipartiteGraph.bipartition_right (m n : ℕ) : (bipartition m n).right = Sum.inr '' Set.Iio n

@[simp]

theorem Graph.CompleteBipartiteGraph.bipartition_left (m n : ℕ) : (bipartition m n).left = Sum.inl '' Set.Iio m

@[simp]

theorem Graph.completeBipartiteGraph_bipartite (m n : ℕ) : (CompleteBipartiteGraph m n).Bipartite

def Graph.completeBipartiteGraphOn {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : Graph (α ⊕ β) (α × β)

A complete-bipartite graph with vertex set a sum type and edge set a product type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.vertexSet_completeBipartiteGraphOn {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : (completeBipartiteGraphOn A B).vertexSet = Sum.inl '' A ∪ Sum.inr '' B

@[simp]

theorem Graph.completeBipartiteGraphOn_isLink {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) (e : α × β) (x y : α ⊕ β) : (completeBipartiteGraphOn A B).IsLink e x y = (x = Sum.inl e.1 ∧ e.1 ∈ A ∧ y = Sum.inr e.2 ∧ e.2 ∈ B ∨ y = Sum.inl e.1 ∧ e.1 ∈ A ∧ x = Sum.inr e.2 ∧ e.2 ∈ B)

@[simp]

theorem Graph.edgeSet_completeBipartiteGraphOn {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : (completeBipartiteGraphOn A B).edgeSet = A ×ˢ B

@[simp]

theorem Graph.completeBipartiteGraphOn_adj_inl_inr_iff {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {x : α} {y : β} : (completeBipartiteGraphOn A B).Adj (Sum.inl x) (Sum.inr y) ↔ x ∈ A ∧ y ∈ B

@[simp]

theorem Graph.completeBipartiteGraphOn_adj_inr_inl_iff {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {x : α} {y : β} : (completeBipartiteGraphOn A B).Adj (Sum.inr y) (Sum.inl x) ↔ x ∈ A ∧ y ∈ B

@[simp]

theorem Graph.completeBipartiteGraphOn_not_adj_inl_inl {α : Type u_1} {β : Type u_2} {x y : α} {A : Set α} {B : Set β} : ¬(completeBipartiteGraphOn A B).Adj (Sum.inl x) (Sum.inl y)

@[simp]

theorem Graph.completeBipartiteGraphOn_not_adj_inr_inr {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {x y : β} : ¬(completeBipartiteGraphOn A B).Adj (Sum.inr x) (Sum.inr y)

@[simp]

theorem Graph.completeBipartiteGraphOn_inc_iff {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {x : α ⊕ β} {e : α × β} : (completeBipartiteGraphOn A B).Inc e x ↔ (e.1 ∈ A ∧ e.2 ∈ B) ∧ (x = Sum.inl e.1 ∨ x = Sum.inr e.2)

@[simp]

instance Graph.completeBipartiteGraphOn_simple {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : (completeBipartiteGraphOn A B).Simple

@[simp]

theorem Graph.completeBipartiteGraphOn_loopless {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : (completeBipartiteGraphOn A B).Loopless

theorem Graph.completeBipartiteGraphOn_map_swap {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : (map Sum.swap (completeBipartiteGraphOn A B)).edgeMap Prod.swap ⋯ = completeBipartiteGraphOn B A

theorem Graph.completeBipartiteGraphOn_eDegree_inl {α : Type u_1} {β : Type u_2} {x : α} {A : Set α} {B : Set β} (hx : x ∈ A) : (completeBipartiteGraphOn A B).eDegree (Sum.inl x) = B.encard

theorem Graph.completeBipartiteGraphOn_eDegree_inr {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {x : β} (hx : x ∈ B) : (completeBipartiteGraphOn A B).eDegree (Sum.inr x) = A.encard

@[simp]

theorem Graph.completeBipartiteGraphOn_empty_left {α : Type u_1} {β : Type u_2} (B : Set β) : completeBipartiteGraphOn ∅ B = noEdge (Sum.inr '' B) (α × β)

@[simp]

theorem Graph.completeBipartiteGraphOn_empty_right {α : Type u_1} {β : Type u_2} (A : Set α) : completeBipartiteGraphOn A ∅ = noEdge (Sum.inl '' A) (α × β)

theorem Graph.completeBipartiteGraphOn_preconnected_iff {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} : (completeBipartiteGraphOn A B).Preconnected ↔ (A = ∅ → B.Subsingleton) ∧ (B = ∅ → A.Subsingleton)

theorem Graph.completeBipartiteGraphOn_connected {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} (hA : A.Nonempty) (hB : B.Nonempty) : (completeBipartiteGraphOn A B).Connected

theorem Graph.completeBipartiteGraphOn_deleteVerts {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) (X : Set (α ⊕ β)) : (completeBipartiteGraphOn A B).deleteVerts X = completeBipartiteGraphOn (A \ Sum.inl ⁻¹' X) (B \ Sum.inr ⁻¹' X)

theorem Graph.completeBipartiteGraphOn_sdiff_left {α : Type u_1} {β : Type u_2} (A X : Set α) (B : Set β) : completeBipartiteGraphOn (A \ X) B = (completeBipartiteGraphOn A B).deleteVerts (Sum.inl '' X)

theorem Graph.completeBipartiteGraphOn_sdiff_right {α : Type u_1} {β : Type u_2} (A : Set α) (B X : Set β) : completeBipartiteGraphOn A (B \ X) = (completeBipartiteGraphOn A B).deleteVerts (Sum.inr '' X)

theorem Graph.completeBipartiteGraphOn_mono_left {α : Type u_1} {A A' : Set α} (hA' : A' ⊆ A) (B : Set α) : (completeBipartiteGraphOn A' B).IsInducedSubgraph (completeBipartiteGraphOn A B)

theorem Graph.completeBipartiteGraphOn_mono_right {α : Type u_1} {β : Type u_2} {B B' : Set β} (A : Set α) (hB' : B' ⊆ B) : (completeBipartiteGraphOn A B').IsInducedSubgraph (completeBipartiteGraphOn A B)