def Graph.«term_↾_» : Lean.TrailingParserDescr

G ↾ F is the subgraph of G restricted to the edges in F. Vertices are not changed.

Equations

• Graph.«term_↾_» = Lean.ParserDescr.trailingNode `Graph.«term_↾_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↾ ") (Lean.ParserDescr.cat `term 66))

def Graph.«term_＼_» : Lean.TrailingParserDescr

G ＼ F is the subgraph of G with the edges in F deleted. Vertices are not changed.

Equations

• Graph.«term_＼_» = Lean.ParserDescr.trailingNode `Graph.«term_＼_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ＼ ") (Lean.ParserDescr.cat `term 76))

def Graph.«term_[_]» : Lean.TrailingParserDescr

G[X] is the subgraph of G induced by the set X of vertices.

Equations

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

theorem Graph.edgeSet_induce_eq_diff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G[X].edgeSet = G.edgeSet \ E(G, G.vertexSet \ X)

@[simp]

theorem Graph.induce_empty {α : Type u_1} {β : Type u_2} (G : Graph α β) : G[∅] = ⊥

def Graph.«term_-_» : Lean.TrailingParserDescr

Equations

• Graph.«term_-_» = Lean.ParserDescr.trailingNode `Graph.«term_-_» 51 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `term 100))

theorem Graph.deleteVerts_def {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G.deleteVerts X = G[G.vertexSet \ X]

@[simp]

theorem Graph.deleteVerts_vertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).vertexSet = G.vertexSet \ X

@[simp]

theorem Graph.deleteVerts_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (G : Graph α β) (X : Set α) : (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X

theorem Graph.deleteVerts_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).edgeSet = {e : β | ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∉ X ∧ y ∉ X}

theorem Graph.deleteVerts_edgeSet_diff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).edgeSet = G.edgeSet \ E(G, X)

@[simp]

theorem Graph.deleteVerts_vertexSet_self {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.deleteVerts G.vertexSet = ⊥

@[simp]

theorem Graph.deleteVerts_singleton_lt {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (h : x ∈ G.vertexSet) : G.deleteVerts {x} < G

theorem Graph.deleteVerts_singleton_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : (G.deleteVerts {x}).edgeSet ∪ E(G, x) = G.edgeSet

theorem Graph.deleteVerts_isLink_iff' {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (G : Graph α β) (X : Set α) : (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ e ∉ E(G, X)

structure Graph.StronglyDisjoint {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Prop

Two graphs are strongly disjoint if their edge sets and vertex sets are disjoint. This is a stronger notion of disjointness than Disjoint, see disjoint_iff_vertexSet_disjoint.

• vertex : Disjoint G.vertexSet H.vertexSet
• edge : Disjoint G.edgeSet H.edgeSet

theorem Graph.stronglyDisjoint_iff {α : Type u_1} {β : Type u_2} (G H : Graph α β) : G.StronglyDisjoint H ↔ Disjoint G.vertexSet H.vertexSet ∧ Disjoint G.edgeSet H.edgeSet

theorem Graph.StronglyDisjoint.symm {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.StronglyDisjoint H) : H.StronglyDisjoint G

instance Graph.StronglyDisjoint.instSymm {α : Type u_1} {β : Type u_2} : Std.Symm StronglyDisjoint

theorem Graph.StronglyDisjoint.anti_left {α : Type u_1} {β : Type u_2} {G H H₁ : Graph α β} (h : G.StronglyDisjoint H) (h₁ : H₁ ≤ G) : H₁.StronglyDisjoint H

theorem Graph.StronglyDisjoint.anti_right {α : Type u_1} {β : Type u_2} {G H H₂ : Graph α β} (h : G.StronglyDisjoint H) (h₂ : H₂ ≤ H) : G.StronglyDisjoint H₂

theorem Graph.StronglyDisjoint.anti {α : Type u_1} {β : Type u_2} {G H H₁ H₂ : Graph α β} (h : G.StronglyDisjoint H) (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ H) : H₁.StronglyDisjoint H₂

theorem Graph.StronglyDisjoint.disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.StronglyDisjoint H) : Disjoint G H

theorem Graph.StronglyDisjoint_iff_of_le_le {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) : H₁.StronglyDisjoint H₂ ↔ Disjoint H₁.vertexSet H₂.vertexSet

theorem Graph.compatible_iff_eqOn {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G.Compatible H ↔ Set.EqOn G.IsLink H.IsLink (G.edgeSet ∩ H.edgeSet)

theorem Graph.Compatible.eqOn {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : Set.EqOn G.IsLink H.IsLink (G.edgeSet ∩ H.edgeSet)

theorem Graph.Compatible.isLink_eq {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (h : G.Compatible H) (heG : e ∈ G.edgeSet) (heH : e ∈ H.edgeSet) : G.IsLink e = H.IsLink e

@[simp]

theorem Graph.compatible_self {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Compatible G

instance Graph.instReflCompatible_matroid {α : Type u_1} {β : Type u_2} : Std.Refl Compatible

instance Graph.instSymmCompatible_matroid {α : Type u_1} {β : Type u_2} : Std.Symm Compatible

@[simp]

theorem Graph.compatible_deleteEdges_right {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G.Compatible (H.deleteEdges G.edgeSet)

@[simp]

theorem Graph.pairwise_compatible_deleteEdges {α : Type u_1} {β : Type u_2} {G H : Graph α β} : {G, H.deleteEdges G.edgeSet}.Pairwise Compatible

Used to simplify the definition of the union of a pair.

@[simp]

theorem Graph.singleEdge_compatible_iff {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} : (Graph.singleEdge u v e).Compatible G ↔ e ∈ G.edgeSet → G.IsLink e u v

def Graph.iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (G : ι → Graph α β) : Graph α β

The intersection of a nonempty family of pairwise compatible graphs. Remove any disagreeing edges.

Equations

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

@[simp]

theorem Graph.vertexSet_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (G : ι → Graph α β) : (Graph.iInter G).vertexSet = ⋂ (i : ι), (G i).vertexSet

@[simp]

theorem Graph.iInter_isLink {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (G : ι → Graph α β) (e : β) (x y : α) : (Graph.iInter G).IsLink e x y = ∀ (i : ι), (G i).IsLink e x y

@[simp]

theorem Graph.edgeSet_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (G : ι → Graph α β) : (Graph.iInter G).edgeSet = {e : β | ∃ (x : α) (y : α), ∀ (i : ι), (G i).IsLink e x y}

theorem Graph.iInter_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : ι → Graph α β} [Nonempty ι] (i : ι) : Graph.iInter G ≤ G i

@[simp]

theorem Graph.le_iInter_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {H : Graph α β} [Nonempty ι] {G : ι → Graph α β} : H ≤ Graph.iInter G ↔ ∀ (i : ι), H ≤ G i

def Graph.sInter {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hne : s.Nonempty) : Graph α β

The intersection of a nonempty set of pairwise compatible graphs.

Equations

• Graph.sInter s hne = Graph.iInter fun (G : ↑s) => ↑G

@[simp]

theorem Graph.vertexSet_sInter {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hne : s.Nonempty) : (Graph.sInter s hne).vertexSet = ⋂ i ∈ s, i.vertexSet

@[simp]

theorem Graph.edgeSet_sInter {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hne : s.Nonempty) : (Graph.sInter s hne).edgeSet = {e : β | ∃ (x : α) (y : α), ∀ a ∈ s, a.IsLink e x y}

@[simp]

theorem Graph.sInter_isLink {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hne : s.Nonempty) (e : β) (x y : α) : (Graph.sInter s hne).IsLink e x y = ∀ a ∈ s, a.IsLink e x y

theorem Graph.sInter_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {Gs : Set (Graph α β)} (hG : G ∈ Gs) : Graph.sInter Gs ⋯ ≤ G

@[simp]

theorem Graph.le_sInter_iff {α : Type u_1} {β : Type u_2} {H : Graph α β} {Gs : Set (Graph α β)} (hne : Gs.Nonempty) : H ≤ Graph.sInter Gs hne ↔ ∀ G ∈ Gs, H ≤ G

def Graph.inter {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Graph α β

The intersection of two graphs G and H. There seems to be no good way to defined junk values so that this has the right edge and vertex set, so the edges are precisely those on which G and H agree, and the edge set is a subset of E(G) ∩ E(H), with equality if G and H are compatible.

Equations

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

@[instance_reducible]

instance Graph.instInter_matroid {α : Type u_1} {β : Type u_2} : Inter (Graph α β)

Equations

• Graph.instInter_matroid = { inter := Graph.inter }

@[simp]

theorem Graph.vertexSet_inter {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G ∩ H).vertexSet = G.vertexSet ∩ H.vertexSet

@[simp]

theorem Graph.inter_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} : (G ∩ H).IsLink e x y ↔ G.IsLink e x y ∧ H.IsLink e x y

theorem Graph.edgeSet_inter {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G ∩ H).edgeSet = {e : β | e ∈ G.edgeSet ∩ H.edgeSet ∧ G.IsLink e = H.IsLink e}

theorem Graph.inter_comm {α : Type u_1} {β : Type u_2} (G H : Graph α β) : G ∩ H = H ∩ G

instance Graph.instCommutativeInter_matroid {α : Type u_1} {β : Type u_2} : Std.Commutative fun (x1 x2 : Graph α β) => x1 ∩ x2

theorem Graph.inter_assoc {α : Type u_1} {β : Type u_2} (G H I : Graph α β) : G ∩ H ∩ I = G ∩ (H ∩ I)

instance Graph.instAssociativeInter_matroid {α : Type u_1} {β : Type u_2} : Std.Associative fun (x1 x2 : Graph α β) => x1 ∩ x2

@[simp]

theorem Graph.inter_le_left {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G ∩ H ≤ G

@[simp]

theorem Graph.inter_le_right {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G ∩ H ≤ H

theorem Graph.le_inter {α : Type u_1} {β : Type u_2} {G₁ G₂ H : Graph α β} (h₁ : H ≤ G₁) (h₂ : H ≤ G₂) : H ≤ G₁ ∩ G₂

@[instance_reducible]

instance Graph.instSemilatticeInf_matroid {α : Type u_1} {β : Type u_2} : SemilatticeInf (Graph α β)

Equations

• Graph.instSemilatticeInf_matroid = { toPartialOrder := Graph.instPartialOrder, inf := Graph.inter, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

def Graph.iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} (G : ι → Graph α β) (hG : Pairwise (Function.onFun Compatible G)) : Graph α β

The union of an indexed family of pairwise compatible graphs.

Equations

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

@[simp]

theorem Graph.vertexSet_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} (G : ι → Graph α β) (hG : Pairwise (Function.onFun Compatible G)) : (Graph.iUnion G hG).vertexSet = ⋃ (i : ι), (G i).vertexSet

@[simp]

theorem Graph.edgeSet_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} (G : ι → Graph α β) (hG : Pairwise (Function.onFun Compatible G)) : (Graph.iUnion G hG).edgeSet = ⋃ (i : ι), (G i).edgeSet

@[simp]

theorem Graph.iUnion_isLink {α : Type u_1} {β : Type u_2} {ι : Type u_3} (G : ι → Graph α β) (hG : Pairwise (Function.onFun Compatible G)) (e : β) (x y : α) : (Graph.iUnion G hG).IsLink e x y = ∃ (i : ι), (G i).IsLink e x y

theorem Graph.le_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (i : ι) : G i ≤ Graph.iUnion G hG

@[simp]

theorem Graph.iUnion_le_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {H : Graph α β} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) : Graph.iUnion G hG ≤ H ↔ ∀ (i : ι), G i ≤ H

def Graph.sUnion {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hs : s.Pairwise Compatible) : Graph α β

The union of a set of pairwise compatible graphs.

Equations

• Graph.sUnion s hs = Graph.iUnion (fun (G : ↑s) => ↑G) ⋯

@[simp]

theorem Graph.vertexSet_sUnion {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hs : s.Pairwise Compatible) : (Graph.sUnion s hs).vertexSet = ⋃ i ∈ s, i.vertexSet

@[simp]

theorem Graph.sUnion_isLink {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hs : s.Pairwise Compatible) (e : β) (x y : α) : (Graph.sUnion s hs).IsLink e x y = ∃ a ∈ s, a.IsLink e x y

@[simp]

theorem Graph.edgeSet_sUnion {α : Type u_1} {β : Type u_2} (s : Set (Graph α β)) (hs : s.Pairwise Compatible) : (Graph.sUnion s hs).edgeSet = ⋃ i ∈ s, i.edgeSet

theorem Graph.le_sUnion {α : Type u_1} {β : Type u_2} {G : Graph α β} {Gs : Set (Graph α β)} (hGs : Gs.Pairwise Compatible) (hG : G ∈ Gs) : G ≤ Graph.sUnion Gs hGs

@[simp]

theorem Graph.bddAbove_deleteEdges {α : Type u_1} {β : Type u_2} {G H : Graph α β} : BddAbove {G, H.deleteEdges G.edgeSet}

Used to simplify the definition of the union of a pair.

@[simp]

theorem Graph.sUnion_le_iff {α : Type u_1} {β : Type u_2} {H : Graph α β} {Gs : Set (Graph α β)} (hGs : Gs.Pairwise Compatible) : Graph.sUnion Gs hGs ≤ H ↔ ∀ G ∈ Gs, G ≤ H

def Graph.union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Graph α β

The union of two graphs G and H. If there is an edge e whose G-ends differ from its H-ends, then G is favoured, so this is not commutative in general. If G and H are Compatible, this doesn't occur. We define this in terms of sUnion and Graph.copy so the vertex and edge sets are definitionally unions.

Equations

• G.union H = (Graph.sUnion {G, H.deleteEdges G.edgeSet} ⋯).copy ⋯ ⋯ ⋯

@[instance_reducible]

instance Graph.instUnion_matroid {α : Type u_1} {β : Type u_2} : Union (Graph α β)

Equations

• Graph.instUnion_matroid = { union := Graph.union }

@[simp]

theorem Graph.vertexSet_union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G ∪ H).vertexSet = G.vertexSet ∪ H.vertexSet

@[simp]

theorem Graph.edgeSet_union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G ∪ H).edgeSet = G.edgeSet ∪ H.edgeSet

theorem Graph.union_eq_sUnion {α : Type u_1} {β : Type u_2} (G H : Graph α β) : G ∪ H = Graph.sUnion {G, H.deleteEdges G.edgeSet} ⋯

theorem Graph.union_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} : (G ∪ H).IsLink e x y ↔ G.IsLink e x y ∨ H.IsLink e x y ∧ e ∉ G.edgeSet

@[simp]

theorem Graph.left_le_union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : G ≤ G ∪ H

theorem Graph.union_le {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) : H₁ ∪ H₂ ≤ G

theorem Graph.union_le_iff {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} : H₁ ∪ H₂ ≤ G ↔ H₁ ≤ G ∧ H₂.deleteEdges H₁.edgeSet ≤ G

@[simp]

theorem Graph.union_self {α : Type u_1} {β : Type u_2} (G : Graph α β) : G ∪ G = G

theorem Graph.union_assoc {α : Type u_1} {β : Type u_2} (G₁ G₂ G₃ : Graph α β) : G₁ ∪ G₂ ∪ G₃ = G₁ ∪ (G₂ ∪ G₃)

instance Graph.instAssociativeUnion_matroid {α : Type u_1} {β : Type u_2} : Std.Associative fun (x1 x2 : Graph α β) => x1 ∪ x2

theorem Graph.Compatible.union_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (h : G.Compatible H) : (G ∪ H).IsLink e x y ↔ G.IsLink e x y ∨ H.IsLink e x y

theorem Graph.Compatible.union_comm {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : G ∪ H = H ∪ G

theorem Graph.Compatible.right_le_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : H ≤ G ∪ H

theorem Graph.Compatible.union_eq_sUnion {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : G ∪ H = Graph.sUnion {G, H} ⋯

theorem Graph.Compatible.union_le_iff {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h_compat : H₁.Compatible H₂) : H₁ ∪ H₂ ≤ G ↔ H₁ ≤ G ∧ H₂ ≤ G

def Graph.addEdge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (a b : α) : Graph α β

Add a new edge e between vertices a and b. If e is already in the graph, its ends change to a and b.

Equations

• G.addEdge e a b = Graph.singleEdge a b e ∪ G

@[simp]

theorem Graph.vertexSet_addEdge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (a b : α) : (G.addEdge e a b).vertexSet = {a, b} ∪ G.vertexSet

@[simp]

theorem Graph.edgeSet_addEdge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (a b : α) : (G.addEdge e a b).edgeSet = insert e G.edgeSet

theorem Graph.addEdge_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {G : Graph α β} [DecidableEq β] {a b : α} : (G.addEdge e a b).IsLink f x y ↔ if f = e then s(a, b) = s(x, y) else G.IsLink f x y

theorem Graph.addEdge_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (a b : α) : (G.addEdge e a b).IsLink e a b

theorem Graph.addEdge_isLink_of_ne {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {G : Graph α β} (hf : G.IsLink f x y) (hne : f ≠ e) (a b : α) : (G.addEdge e a b).IsLink f x y

theorem Graph.addEdge_isLink_iff_of_notMem {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {G : Graph α β} {a b : α} (he : e ∉ G.edgeSet) : (G.addEdge e a b).IsLink f x y ↔ f = e ∧ s(a, b) = s(x, y) ∨ G.IsLink f x y

theorem Graph.addEdge_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (a b : α) : G.addEdge e a b = G.addEdge e b a

theorem Graph.addEdge_le {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hle : H ≤ G) (he : G.IsLink e x y) : H.addEdge e x y ≤ G

theorem Graph.le_addEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) : G ≤ G.addEdge e x y

theorem Graph.addEdge_eq_self {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (hbtw : G.IsLink e x y) : G.addEdge e x y = G

theorem Graph.addEdge_idem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : (G.addEdge e x y).addEdge e x y = G.addEdge e x y