Documentation

Matroid.Graph.Subgraph.Union

Indexed unions #

@[simp]

theorem Graph.iUnion_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (G : Graph α β) :

Graph.iUnion (fun (x : ι) => G) ⋯ = G

@[simp]

theorem Graph.iUnion_inc_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : α} {e : β} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) :

(Graph.iUnion G hG).Inc e x ↔ ∃ (i : ι), (G i).Inc e x

@[simp]

theorem Graph.iUnion_isLoopAt_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : α} {e : β} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) :

(Graph.iUnion G hG).IsLoopAt e x ↔ ∃ (i : ι), (G i).IsLoopAt e x

@[simp]

theorem Graph.iUnion_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : α} {e : β} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) :

(Graph.iUnion G hG).IsNonloopAt e x ↔ ∃ (i : ι), (G i).IsNonloopAt e x

theorem Graph.iUnion_map_le_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (f : ι' → ι) :

Graph.iUnion (G ∘ f) ⋯ ≤ Graph.iUnion G hG

theorem Graph.iUnion_left_le_iUnion_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : ι → Graph α β} {H : ι' → Graph α β} (hGH : Pairwise (Function.onFun Compatible (Sum.elim G H))) :

Graph.iUnion G ⋯ ≤ Graph.iUnion (Sum.elim G H) hGH

theorem Graph.iUnion_right_le_iUnion_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : ι → Graph α β} {H : ι' → Graph α β} (hGH : Pairwise (Function.onFun Compatible (Sum.elim G H))) :

Graph.iUnion H ⋯ ≤ Graph.iUnion (Sum.elim G H) hGH

@[simp]

theorem Graph.induce_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (X : Set α) :

(Graph.iUnion G hG)[X] = Graph.iUnion (fun (i : ι) => (G i)[X]) ⋯

@[simp]

theorem Graph.Compatible.deleteVerts_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (X : Set α) :

(Graph.iUnion G hG).deleteVerts X = Graph.iUnion (fun (i : ι) => (G i).deleteVerts X) ⋯

@[simp]

theorem Graph.Compatible.deleteEdges_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (F : Set β) :

(Graph.iUnion G hG).deleteEdges F = Graph.iUnion (fun (i : ι) => (G i).deleteEdges F) ⋯

@[simp]

theorem Graph.Compatible.restrict_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (F : Set β) :

(Graph.iUnion G hG).restrict F = Graph.iUnion (fun (i : ι) => (G i).restrict F) ⋯

theorem Graph.iUnion_comp_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {f : ι' → ι} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) :

Graph.iUnion (fun (i : ι') => G (f i)) ⋯ ≤ Graph.iUnion G hG

theorem Graph.iUnion_comp_eq_of_surj {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {f : ι' → ι} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (hf : Function.Surjective f) :

Graph.iUnion G hG = Graph.iUnion (fun (i : ι') => G (f i)) ⋯

theorem Graph.iUnion_range {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {f : ι' → ι} {G : ↑(Set.range f) → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) :

Graph.iUnion G hG = Graph.iUnion (fun (x : ι') => G (Set.rangeFactorization f x)) ⋯

Set unions #

@[simp]

theorem Graph.sUnion_inc_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Gs : Set (Graph α β)} (hGs : Gs.Pairwise Compatible) :

(Graph.sUnion Gs hGs).Inc e x ↔ ∃ G ∈ Gs, G.Inc e x

@[simp]

theorem Graph.sUnion_isLoopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Gs : Set (Graph α β)} (hGs : Gs.Pairwise Compatible) :

(Graph.sUnion Gs hGs).IsLoopAt e x ↔ ∃ G ∈ Gs, G.IsLoopAt e x

@[simp]

theorem Graph.sUnion_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Gs : Set (Graph α β)} (hGs : Gs.Pairwise Compatible) :

(Graph.sUnion Gs hGs).IsNonloopAt e x ↔ ∃ G ∈ Gs, G.IsNonloopAt e x

@[simp]

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

Graph.sUnion {G} ⋯ = G

theorem Graph.sUnion_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {s : Set ι} {f : ι → Graph α β} (hs : s.Pairwise (Function.onFun Compatible f)) :

Graph.sUnion (f '' s) ⋯ = Graph.iUnion (fun (x : ↑s) => f ↑x) ⋯

theorem Graph.sUnion_range {α : Type u_1} {β : Type u_2} {ι : Type u_3} {f : ι → Graph α β} (h : Pairwise (Function.onFun Compatible f)) :

Graph.sUnion (Set.range f) ⋯ = Graph.iUnion f h

Unions of pairs #

theorem Graph.union_inc_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} :

(G ∪ H).Inc e x ↔ G.Inc e x ∨ H.Inc e x ∧ e ∉ G.edgeSet

theorem Graph.union_isLoopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} :

(G ∪ H).IsLoopAt e x ↔ G.IsLoopAt e x ∨ H.IsLoopAt e x ∧ e ∉ G.edgeSet

theorem Graph.union_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} :

(G ∪ H).IsNonloopAt e x ↔ G.IsNonloopAt e x ∨ H.IsNonloopAt e x ∧ e ∉ G.edgeSet

theorem Graph.union_eq_union_deleteEdges {α : Type u_1} {β : Type u_2} (G H : Graph α β) :

G ∪ H = G ∪ H.deleteEdges G.edgeSet

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

G ∪ H₁ ≤ G ∪ H₂

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

G.IsLink e x y ∨ H.IsLink e x y

theorem Graph.restrict_union {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) :

G.restrict (F₁ ∪ F₂) = G.restrict F₁ ∪ G.restrict F₂

theorem Graph.Compatible.union_inc_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : G.Compatible H) :

(G ∪ H).Inc e x ↔ G.Inc e x ∨ H.Inc e x

theorem Graph.Compatible.union_isLoopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : G.Compatible H) :

(G ∪ H).IsLoopAt e x ↔ G.IsLoopAt e x ∨ H.IsLoopAt e x

theorem Graph.Compatible.union_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : G.Compatible H) :

(G ∪ H).IsNonloopAt e x ↔ G.IsNonloopAt e x ∨ H.IsNonloopAt e x

theorem Graph.Compatible.union_adj_iff {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (h : G.Compatible H) :

(G ∪ H).Adj x y ↔ G.Adj x y ∨ H.Adj x y

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

G ∪ H = H

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

H ∪ G = H

@[simp]

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

@[simp]

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

@[simp]

theorem Graph.union_eq_bot {α : Type u_1} {β : Type u_2} {G H : Graph α β} :

G ∪ H = ⊥ ↔ G = ⊥ ∧ H = ⊥

theorem Graph.Compatible.union_mono_left {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h : H₂.Compatible G) (hle : H₁ ≤ H₂) :

H₁ ∪ G ≤ H₂ ∪ G

theorem Graph.compatible_iff_exists_le_le {α : Type u_1} {β : Type u_2} (G H : Graph α β) :

G.Compatible H ↔ ∃ (I : Graph α β), G ≤ I ∧ H ≤ I

theorem Graph.bddAbove_iff_pairwise_compatible {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} :

BddAbove Gs ↔ Gs.Pairwise Compatible

theorem Graph.Compatible.union_mono {α : Type u_1} {β : Type u_2} {G₁ G₂ H₁ H₂ : Graph α β} (hleG : G₁ ≤ G₂) (hleH : H₁ ≤ H₂) (h : G₂.Compatible H₁) :

G₁ ∪ H₁ ≤ G₂ ∪ H₂

theorem Graph.restrict_union_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) :

G.restrict F ∪ G.deleteEdges F = G

theorem Graph.deleteEdges_union_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) :

G.deleteEdges F ∪ G.restrict F = G

theorem Graph.induce_union_deleteEdges {α : Type u_1} {β : Type u_2} {X : Set α} (G : Graph α β) (hX : X ⊆ G.vertexSet) :

G[X] ∪ G.deleteEdges G[X].edgeSet = G

theorem Graph.deleteEdges_union_induce {α : Type u_1} {β : Type u_2} {X : Set α} (G : Graph α β) (hX : X ⊆ G.vertexSet) :

G.deleteEdges G[X].edgeSet ∪ G[X] = G

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

G ∪ H = Graph.iUnion (fun (b : Bool) => bif b then G else H) ⋯

theorem Graph.Compatible.induce_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (X : Set α) :

(G ∪ H)[X] = G[X] ∪ H[X]

theorem Graph.Compatible.deleteVerts_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (X : Set α) :

(G ∪ H).deleteVerts X = G.deleteVerts X ∪ H.deleteVerts X

theorem Graph.induce_union {α : Type u_1} {β : Type u_2} (G : Graph α β) (X Y : Set α) (hX : ∀ x ∈ X, ∀ y ∈ Y, ¬G.Adj x y) :

G[X ∪ Y] = G[X] ∪ G[Y]

theorem Graph.inter_distrib_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {H : ι → Graph α β} (hH : Pairwise (Function.onFun Compatible H)) :

G ∩ Graph.iUnion H hH = Graph.iUnion (fun (i : ι) => G ∩ H i) ⋯

theorem Graph.inter_distrib_sUnion {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} {G : Graph α β} (hs : Gs.Pairwise Compatible) :

G ∩ Graph.sUnion Gs hs = Graph.sUnion ((fun (K : Graph α β) => G ∩ K) '' Gs) ⋯

theorem Graph.Pairwise.union_compatible {α : Type u_1} {β : Type u_2} {s t : Set (Graph α β)} (hst : (s ∪ t).Pairwise Compatible) :

(Graph.sUnion s ⋯).Compatible (Graph.sUnion t ⋯)

theorem Graph.sUnion_union_sUnion {α : Type u_1} {β : Type u_2} {s t : Set (Graph α β)} (hst : (s ∪ t).Pairwise Compatible) :

Graph.sUnion s ⋯ ∪ Graph.sUnion t ⋯ = Graph.sUnion (s ∪ t) hst

theorem Graph.Compatible.sum_compatible {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : ι → Graph α β} {H : ι' → Graph α β} (hGH : Pairwise (Function.onFun Compatible (Sum.elim G H))) :

(Graph.iUnion G ⋯).Compatible (Graph.iUnion H ⋯)

theorem Graph.iUnion_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Nonempty ι] [Nonempty ι'] {G : ι → Graph α β} {H : ι' → Graph α β} (hGH : Pairwise (Function.onFun Compatible (Sum.elim G H))) :

Graph.iUnion (Sum.elim G H) hGH = Graph.iUnion G ⋯ ∪ Graph.iUnion H ⋯

theorem Graph.Compatible.edgeSet_inter_eq_loopSet_of_inter_eq_singleton {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (hcompat : G.Compatible H) (hi : G.vertexSet ∩ H.vertexSet = {x}) :

G.edgeSet ∩ H.edgeSet = loopSet x ∩ H.edgeSet

theorem Graph.Compatible.edgeSet_inter_subset_loopSet_union {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (hcompat : G.Compatible H) (hx : G.vertexSet ∩ H.vertexSet = {x}) :

G.edgeSet ∩ H.edgeSet ⊆ loopSet x

Subgraphs #

theorem Graph.pairwise_compatible_of_subgraph {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {H : ι → Graph α β} (h : ∀ (i : ι), H i ≤ G) :

Pairwise (Function.onFun Compatible H)

theorem Graph.set_pairwise_compatible_of_subgraph {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} {G : Graph α β} (h : ∀ ⦃H : Graph α β⦄, H ∈ Gs → H ≤ G) :

Gs.Pairwise Compatible

theorem Graph.iUnion_le_of_forall_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {H : ι → Graph α β} (h : ∀ (i : ι), H i ≤ G) :

Graph.iUnion H ⋯ ≤ G

theorem Graph.sUnion_le_of_forall_le {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} {G : Graph α β} (h : ∀ ⦃H : Graph α β⦄, H ∈ Gs → H ≤ G) :

Graph.sUnion Gs ⋯ ≤ G

theorem Graph.iUnion_isClosedSubgraph {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {H : ι → Graph α β} (h : ∀ (i : ι), (H i).IsClosedSubgraph G) :

(Graph.iUnion H ⋯).IsClosedSubgraph G

A union of closed subgraphs of G is a closed subgraph of G.

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

Graph.iUnion H ⋯ ≤s G

A nonempty union of spanning subgraphs of G is a spanning subgraph of G.

theorem Graph.iUnion_isSpanningSubgraph_of_exists_isSpanningSubgraph_of_forall_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {H : ι → Graph α β} [Nonempty ι] (h : ∀ (i : ι), H i ≤ G) (hH : ∃ (i : ι), H i ≤s G) :

Graph.iUnion H ⋯ ≤s G

theorem Graph.sUnion_isClosedSubgraph {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} {G : Graph α β} (hs : ∀ ⦃H : Graph α β⦄, H ∈ Gs → H.IsClosedSubgraph G) :

(Graph.sUnion Gs ⋯).IsClosedSubgraph G

theorem Graph.sUnion_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} {G : Graph α β} (hs : ∀ ⦃H : Graph α β⦄, H ∈ Gs → H ≤s G) (hne : Gs.Nonempty) :

Graph.sUnion Gs ⋯ ≤s G