Matroid.Graph.Subgraph.Inter

Indexed Intersections #

@[simp]

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

(Graph.iInter fun (x : ι) => G) = G

theorem Graph.iInter_comp_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Nonempty ι] [Nonempty ι'] {f : ι' → ι} {G : ι → Graph α β} :

Graph.iInter G ≤ Graph.iInter fun (i : ι') => G (f i)

source

theorem Graph.iInter_comp_eq_of_surj {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Nonempty ι] [Nonempty ι'] {f : ι' → ι} {G : ι → Graph α β} (hf : Function.Surjective f) :

Graph.iInter G = Graph.iInter fun (i : ι') => G (f i)

source

theorem Graph.iInter_range {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Nonempty ι'] {f : ι' → ι} {G : ↑(Set.range f) → Graph α β} :

Graph.iInter G = Graph.iInter fun (i : ι') => G (Set.rangeFactorization f i)

source

@[simp]

theorem Graph.iInter_inc_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : α} {e : β} [Nonempty ι] {G : ι → Graph α β} :

(Graph.iInter G).Inc e x ↔ ∃ (y : α), ∀ (i : ι), (G i).IsLink e x y

source

@[simp]

theorem Graph.iInter_isLoopAt_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : α} {e : β} [Nonempty ι] {G : ι → Graph α β} :

(Graph.iInter G).IsLoopAt e x ↔ ∀ (i : ι), (G i).IsLoopAt e x

source

@[simp]

theorem Graph.iInter_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : α} {e : β} [Nonempty ι] {G : ι → Graph α β} :

(Graph.iInter G).IsNonloopAt e x ↔ ∃ (y : α), y ≠ x ∧ ∀ (i : ι), (G i).IsLink e x y

source

@[simp]

theorem Graph.induce_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {G : ι → Graph α β} (X : Set α) :

(Graph.iInter G)[X] = Graph.iInter fun (i : ι) => (G i)[X]

source

@[simp]

theorem Graph.deleteVerts_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {G : ι → Graph α β} (X : Set α) :

(Graph.iInter G).deleteVerts X = Graph.iInter fun (i : ι) => (G i).deleteVerts X

source

@[simp]

theorem Graph.deleteEdges_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {G : ι → Graph α β} (F : Set β) :

(Graph.iInter G).deleteEdges F = Graph.iInter fun (i : ι) => (G i).deleteEdges F

source

@[simp]

theorem Graph.restrict_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {G : ι → Graph α β} (F : Set β) :

(Graph.iInter G).restrict F = Graph.iInter fun (i : ι) => (G i).restrict F

Set Intersections #

source

theorem Graph.sInter_anti {α : Type u_1} {β : Type u_2} {Gs Hs : Set (Graph α β)} (hne : Gs.Nonempty) (hne' : Hs.Nonempty) (hle : Gs ⊆ Hs) :

Graph.sInter Hs hne' ≤ Graph.sInter Gs hne

source

def Graph.Equiv.insert_option {α : Type u_1} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (a : α) (has : a ∉ s) :

Option ↑s ≃ ↑(insert a s)

Equations

Graph.Equiv.insert_option a has = (Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm

Instances For

source

theorem Graph.sInter_insert_eq_iInter {α : Type u_1} {β : Type u_2} {G : Graph α β} {Gs : Set (Graph α β)} [DecidablePred fun (x : Graph α β) => x ∈ Gs] (hGs : G ∉ Gs) :

Graph.sInter (insert G Gs) ⋯ = Graph.iInter ((fun (G_1 : ↑(insert G Gs)) => ↑G_1) ∘ ⇑(Equiv.insert_option G hGs))

source

theorem Graph.sInter_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {s : Set ι} (hne : s.Nonempty) (f : ι → Graph α β) :

Graph.sInter (f '' s) ⋯ = Graph.iInter fun (x : ↑s) => f ↑x

source

theorem Graph.sInter_range {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {f : ι → Graph α β} :

Graph.sInter (Set.range f) ⋯ = Graph.iInter f

source

@[simp]

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

Graph.sInter {G} ⋯ = G

source

@[simp]

theorem Graph.sInter_inc_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) :

(Graph.sInter Gs hs).Inc e x ↔ ∃ (y : α), ∀ G ∈ Gs, G.IsLink e x y

source

@[simp]

theorem Graph.sInter_isLoopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) :

(Graph.sInter Gs hs).IsLoopAt e x ↔ ∀ G ∈ Gs, G.IsLoopAt e x

source

@[simp]

theorem Graph.sInter_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) :

(Graph.sInter Gs hs).IsNonloopAt e x ↔ ∃ (y : α), y ≠ x ∧ ∀ G ∈ Gs, G.IsLink e x y

source

@[simp]

theorem Graph.induce_sInter {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) (X : Set α) :

(Graph.sInter Gs hs)[X] = Graph.sInter ((fun (x : Graph α β) => x[X]) '' Gs) ⋯

source

@[simp]

theorem Graph.deleteVerts_sInter {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) (X : Set α) :

(Graph.sInter Gs hs).deleteVerts X = Graph.sInter ((fun (x : Graph α β) => x.deleteVerts X) '' Gs) ⋯

source

@[simp]

theorem Graph.deleteEdges_sInter {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) (F : Set β) :

(Graph.sInter Gs hs).deleteEdges F = Graph.sInter ((fun (x : Graph α β) => x.deleteEdges F) '' Gs) ⋯

source

@[simp]

theorem Graph.restrict_sInter {α : Type u_1} {β : Type u_2} {Gs : Set (Graph α β)} (hs : Gs.Nonempty) (F : Set β) :

(Graph.sInter Gs hs).restrict F = Graph.sInter ((fun (x : Graph α β) => x.restrict F) '' Gs) ⋯

Intersections #

source

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

(G ∩ H).edgeSet ⊆ G.edgeSet ∩ H.edgeSet

source

@[simp]

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

(G ∩ H).Inc e x ↔ ∃ (y : α), G.IsLink e x y ∧ H.IsLink e x y

source

@[simp]

theorem Graph.inter_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

source

@[simp]

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

(G ∩ H).IsNonloopAt e x ↔ ∃ (y : α), y ≠ x ∧ G.IsLink e x y ∧ H.IsLink e x y

source

@[simp]

theorem Graph.inf_eq_inter {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} :

H₁ ⊓ H₂ = H₁ ∩ H₂

source

@[simp]

theorem Graph.inter_eq_bot_iff {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} :

H₁ ∩ H₂ = ⊥ ↔ H₁.vertexSet ∩ H₂.vertexSet = ∅

source

theorem Graph.disjoint_iff_inter_eq_bot {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} :

Disjoint H₁ H₂ ↔ H₁ ∩ H₂ = ⊥

source

@[simp]

theorem Graph.disjoint_iff_vertexSet_inter_eq_empty {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} :

Disjoint H₁ H₂ ↔ H₁.vertexSet ∩ H₂.vertexSet = ∅

source

theorem Graph.disjoint_iff_vertexSet_disjoint {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} :

Disjoint H₁ H₂ ↔ Disjoint H₁.vertexSet H₂.vertexSet

source

theorem Graph.Disjoint.vertex_disjoint {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} :

Disjoint H₁ H₂ → Disjoint H₁.vertexSet H₂.vertexSet

Alias of the forward direction of Graph.disjoint_iff_vertexSet_disjoint.

source

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

(G ∩ H).edgeSet = G.edgeSet ∩ H.edgeSet

source

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

G ∩ H = Graph.iInter fun (b : Bool) => bif b then G else H

source

theorem Graph.le_inter_iff {α : Type u_1} {β : Type u_2} {G₁ G₂ H : Graph α β} :

H ≤ G₁ ∩ G₂ ↔ H ≤ G₁ ∧ H ≤ G₂

source

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

G ∩ H = G

source

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

G ≤ H

source

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

G₁ ∩ H ≤ G₂ ∩ H

source

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

G ∩ H₁ ≤ G ∩ H₂

source

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

G₁ ∩ H₁ ≤ G₂ ∩ H₂

source

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

G.edgeSet ∩ H[X].edgeSet = G[X].edgeSet

source

theorem Graph.induce_inter {α : Type u_1} {β : Type u_2} {G : Graph α β} (X Y : Set α) :

G[X ∩ Y] = G[X] ∩ G[Y]

source

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

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

source

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

G.deleteVerts (X ∪ Y) = G.deleteVerts X ∩ G.deleteVerts Y

source

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

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

source

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

G.deleteEdges (F₁ ∪ F₂) = G.deleteEdges F₁ ∩ G.deleteEdges F₂

source

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

(G ∩ H).deleteEdges F = G.deleteEdges F ∩ H.deleteEdges F

source

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

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

source

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

(G ∩ H).restrict F = G.restrict F ∩ H.restrict F

source

theorem Graph.inter_distrib_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} [Nonempty ι] {H : ι → Graph α β} :

G ∩ Graph.iInter H = Graph.iInter fun (i : ι) => G ∩ H i

source

theorem Graph.inter_distrib_sInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} [Nonempty ι] {s : Set (Graph α β)} (hne : s.Nonempty) :

G ∩ Graph.sInter s hne = Graph.sInter ((fun (x : Graph α β) => G ∩ x) '' s) ⋯

source

theorem Graph.sInter_inter_sInter {α : Type u_1} {β : Type u_2} {s t : Set (Graph α β)} (hs : s.Nonempty) (ht : t.Nonempty) :

Graph.sInter s hs ∩ Graph.sInter t ht = Graph.sInter (s ∪ t) ⋯

source

theorem Graph.iInter_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Nonempty ι] [Nonempty ι'] {G : ι → Graph α β} {H : ι' → Graph α β} :

Graph.iInter (Sum.elim G H) = Graph.iInter G ∩ Graph.iInter H

source

theorem Graph.iInter_option {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {G₁ : Graph α β} {G : ι → Graph α β} :

(Graph.iInter fun (x : Option ι) => x.elim G₁ G) = G₁ ∩ Graph.iInter G

source

theorem Graph.sInter_insert {α : Type u_1} {β : Type u_2} {s : Set (Graph α β)} (G : Graph α β) (hne : s.Nonempty) :

Graph.sInter (insert G s) ⋯ = G ∩ Graph.sInter s hne

source

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

Graph.iInter Hι ≤ G

source

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

Graph.sInter Gs hne ≤ G

source

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

(Graph.iInter Hι).IsInducedSubgraph G

A nonempty intersection of induced subgraphs G is an induced subgraph of G

source

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

Graph.iInter Hι ≤s G

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

source

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

(Graph.iInter Hι).IsClosedSubgraph G

A nonempty intersection of closed subgraphs G is an induced subgraph of G

source

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

(Graph.sInter Gs hne).IsInducedSubgraph G

source

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

(Graph.sInter Gs hne).IsClosedSubgraph G