Components

theorem Graph.IsCompOf.ne_bot {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHco : H.IsCompOf G) : H ≠ ⊥

@[simp]

theorem Graph.bot_not_isCompOf {α : Type u_1} {β : Type u_2} {G : Graph α β} : ¬⊥.IsCompOf G

@[simp]

theorem Graph.not_isCompOf_bot {α : Type u_1} {β : Type u_2} {G : Graph α β} : ¬G.IsCompOf ⊥

theorem Graph.IsClosedSubgraph.le_isCompOf_iff {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hH₁cl : H₁.IsClosedSubgraph G) (hH₂co : H₂.IsCompOf G) : H₁ ≤ H₂ ↔ H₁ = ⊥ ∨ H₁ = H₂

theorem Graph.IsClosedSubgraph.lt_isCompOf_iff {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hH₁cl : H₁.IsClosedSubgraph G) (hH₂co : H₂.IsCompOf G) : H₁ < H₂ ↔ H₁ = ⊥

theorem Graph.IsClosedSubgraph.eq_of_le_isCompOf_of_vertexSet_not_disjoint {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hH₁cl : H₁.IsClosedSubgraph G) (hH₂co : H₂.IsCompOf G) (hle : H₁ ≤ H₂) (hV : ¬Disjoint H₁.vertexSet H₂.vertexSet) : H₁ = H₂

theorem Graph.IsCompOf.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H H' : Graph α β} (hHcl : H.IsClosedSubgraph G) (hH'co : H'.IsCompOf H) : H'.IsCompOf G

def Graph.walkable {α : Type u_1} {β : Type u_2} (G : Graph α β) (u : α) : Graph α β

Equations

• G.walkable u = G[{x : α | G.ConnBetween u x}]

theorem Graph.mem_walkable {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : x ∈ (G.walkable x).vertexSet

@[simp]

theorem Graph.mem_walkable_iff {α : Type u_1} {β : Type u_2} {u x : α} {G : Graph α β} : x ∈ (G.walkable u).vertexSet ↔ G.ConnBetween u x

theorem Graph.walkable_isClosedSubgraph {α : Type u_1} {β : Type u_2} {u : α} {G : Graph α β} : (G.walkable u).IsClosedSubgraph G

theorem Graph.Adj.mem_walkable {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : y ∈ (G.walkable x).vertexSet

@[simp]

theorem Graph.mem_walkable_self_iff {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} : x ∈ (G.walkable x).vertexSet ↔ x ∈ G.vertexSet

@[simp]

theorem Graph.walkable_eq_bot {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∉ G.vertexSet) : G.walkable x = ⊥

theorem Graph.exists_isWalk_of_mem_mem {α : Type u_1} {β : Type u_2} {u x y : α} {G : Graph α β} (hx : x ∈ (G.walkable u).vertexSet) (hy : y ∈ (G.walkable u).vertexSet) : ∃ (W : WList α β), G.IsWalk W ∧ W.first = x ∧ W.last = y

theorem Graph.mem_walkable_symm {α : Type u_1} {β : Type u_2} {u x : α} {G : Graph α β} (hx : x ∈ (G.walkable u).vertexSet) : u ∈ (G.walkable x).vertexSet

theorem Graph.mem_walkable_comm {α : Type u_1} {β : Type u_2} {u x : α} {G : Graph α β} : x ∈ (G.walkable u).vertexSet ↔ u ∈ (G.walkable x).vertexSet

theorem Graph.mem_walkable_trans {α : Type u_1} {β : Type u_2} {u v x : α} {G : Graph α β} (huv : u ∈ (G.walkable v).vertexSet) (hvx : v ∈ (G.walkable x).vertexSet) : u ∈ (G.walkable x).vertexSet

theorem Graph.walkable_eq_walkable_of_mem {α : Type u_1} {β : Type u_2} {u x : α} {G : Graph α β} (hx : x ∈ (G.walkable u).vertexSet) : G.walkable x = G.walkable u

@[simp]

theorem Graph.walkable_eq_walkable_iff_mem {α : Type u_1} {β : Type u_2} {u x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : G.walkable x = G.walkable u ↔ x ∈ (G.walkable u).vertexSet

theorem Graph.IsClosedSubgraph.walkable_le_of_mem {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (hcl : H.IsClosedSubgraph G) (hx : x ∈ H.vertexSet) : G.walkable x ≤ H

theorem Graph.walkable_isCompOf {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : (G.walkable x).IsCompOf G

theorem Graph.exists_IsCompOf {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : ∃ (H : Graph α β), H.IsCompOf G

theorem Graph.IsCompOf.eq_walkable_of_mem_walkable {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (hHco : H.IsCompOf G) (hx : x ∈ H.vertexSet) : H = G.walkable x

theorem Graph.isCompOf_iff_exists_walkable {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsCompOf G ↔ ∃ x ∈ H.vertexSet, G.walkable x = H

theorem Graph.IsCompOf.exists_walkable {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsCompOf G → ∃ x ∈ H.vertexSet, G.walkable x = H

Alias of the forward direction of Graph.isCompOf_iff_exists_walkable.

theorem Graph.exists_IsCompOf_vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : ∃ (H : Graph α β), H.IsCompOf G ∧ x ∈ H.vertexSet

theorem Graph.IsCompOf.le_of_mem_mem {α : Type u_1} {β : Type u_2} {x : α} {G H₁ H₂ : Graph α β} (hH₁ : H₁.IsCompOf G) (hH₂cl : H₂.IsClosedSubgraph G) (hx₁ : x ∈ H₁.vertexSet) (hx₂ : x ∈ H₂.vertexSet) : H₁ ≤ H₂

theorem Graph.IsCompOf.eq_of_not_disjoint {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hH₁co : H₁.IsCompOf G) (hH₂co : H₂.IsCompOf G) (hV : ¬Disjoint H₁.vertexSet H₂.vertexSet) : H₁ = H₂

theorem Graph.IsCompOf.not_disjoint_iff {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hH₁co : H₁.IsCompOf G) (hH₂co : H₂.IsCompOf G) : ¬Disjoint H₁.vertexSet H₂.vertexSet ↔ H₁ = H₂

def Graph.Components {α : Type u_1} {β : Type u_2} (G : Graph α β) : Set (Graph α β)

Equations

• G.Components = {H : Graph α β | H.IsCompOf G}

noncomputable def Graph.NumberOfComponents {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ∞

Equations

• c(G) = G.Components.encard

def Graph.«termC(_)» : Lean.ParserDescr

Equations

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

def Graph.compPartition {α : Type u_1} {β : Type u_2} (G : Graph α β) : Partition G.Subgraph

Equations

• G.compPartition = Partition.ofPairwiseDisjoint' ⋯ ⋯

@[simp]

theorem Graph.compPartition_parts {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.compPartition.parts = {H : G.Subgraph | (↑H).IsCompOf G}

@[simp]

theorem Graph.compPartition_parts_eq_components {α : Type u_1} {β : Type u_2} (G : Graph α β) : Subtype.val '' G.compPartition.parts = G.Components

@[simp]

theorem Graph.mem_components_iff_isCompOf {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H ∈ G.Components ↔ H.IsCompOf G

@[simp]

theorem Graph.mem_compPartition_iff_isCompOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {H : G.Subgraph} : H ∈ G.compPartition ↔ (↑H).IsCompOf G

@[simp]

theorem Graph.bot_notMem_components {α : Type u_1} {β : Type u_2} (G : Graph α β) : ⊥ ∉ G.Components

def Graph.connPartition {α : Type u_1} {β : Type u_2} (G : Graph α β) : Partition (Set α)

Equations

• G.connPartition = { parts := (fun (x : Graph α β) => x.vertexSet) '' G.Components, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Graph.connPartition_parts {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.connPartition.parts = (fun (x : Graph α β) => x.vertexSet) '' G.Components

theorem Graph.mem_connPartition_iff_isCompOf {α : Type u_1} {β : Type u_2} {S : Set α} {G : Graph α β} : S ∈ G.connPartition ↔ ∃ (H : Graph α β), H.IsCompOf G ∧ H.vertexSet = S

@[simp]

theorem Graph.IsCompOf.mem_connPartition {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHco : H.IsCompOf G) : H.vertexSet ∈ G.connPartition

@[simp]

theorem Graph.induce_connPartition_parts_eq_components {α : Type u_1} {β : Type u_2} (G : Graph α β) : (fun (x : Set α) => G[x]) '' G.connPartition.parts = G.Components

@[simp]

theorem Graph.connPartition_supp {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.connPartition.supp = G.vertexSet

theorem Graph.components_pairwise_stronglyDisjoint {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Components.Pairwise StronglyDisjoint

theorem Graph.components_pairwise_disjoint {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Components.Pairwise Disjoint

theorem Graph.components_pairwise_compatible {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Components.Pairwise Compatible

theorem Graph.eq_sUnion_components {α : Type u_1} {β : Type u_2} (G : Graph α β) : G = Graph.sUnion G.Components ⋯

@[simp]

theorem Graph.components_eq_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Components = ∅ ↔ G = ⊥

theorem Graph.components_nonempty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Components.Nonempty ↔ G.vertexSet.Nonempty

theorem Graph.components_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.vertexSet.Nonempty → G.Components.Nonempty

Alias of the reverse direction of Graph.components_nonempty_iff.

theorem Graph.exists_isCompOf_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : (∃ (H : Graph α β), H.IsCompOf G) ↔ G.vertexSet.Nonempty

theorem Graph.exists_isCompOf {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.vertexSet.Nonempty → ∃ (H : Graph α β), H.IsCompOf G

Alias of the reverse direction of Graph.exists_isCompOf_iff.

theorem Graph.components_eq_walkable_image {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Components = G.walkable '' G.vertexSet

theorem Graph.components_encard_le {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Components.encard ≤ G.vertexSet.encard

@[simp]

theorem Graph.biUnion_components_vertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : ⋃ H ∈ G.Components, H.vertexSet = G.vertexSet

@[simp]

theorem Graph.biUnion_components_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : ⋃ H ∈ G.Components, H.edgeSet = G.edgeSet

theorem Graph.IsClosedSubgraph.components_subset_components {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hcl : H.IsClosedSubgraph G) : H.Components ⊆ G.Components

def Graph.ClosedSubgraph.orderIso_set_components {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.ClosedSubgraph ≃o Set ↑{a : G.ClosedSubgraph | IsAtom a}

Equations

• Graph.ClosedSubgraph.orderIso_set_components G = CompleteAtomicBooleanAlgebra.toSetOfIsAtom

@[simp]

theorem Graph.ClosedSubgraph.orderIso_set_components_sSup {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) : sSup (Subtype.val '' (orderIso_set_components G) H) = H

theorem Graph.ClosedSubgraph.le_of_mem_orderIso_set_components {α : Type u_1} {β : Type u_2} {G : Graph α β} (H H' : G.ClosedSubgraph) : H' ∈ Subtype.val '' (orderIso_set_components G) H → H' ≤ H