Matroid.Graph.Subgraph.Compatible

@[simp]

theorem Option.elim_eq_const_of_isEmpty {β : Type u_2} {α : Type u_5} [hα : IsEmpty α] (f : α → β) (b : β) :

(fun (x : Option α) => x.elim b f) = fun (x : Option α) => b

Strongly disjointness #

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

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

Instances For

source

theorem Graph.stronglyDisjoint_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G H : Graph α β) :

G.StronglyDisjoint H ↔ Disjoint G.vertexSet H.vertexSet ∧ Disjoint G.edgeSet H.edgeSet

source

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

H.StronglyDisjoint G

source

theorem Graph.StronglyDisjoint_iff_of_le_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) :

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

source

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

Disjoint G H

Compatibility #

source

def Graph.CompatibleAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] (e : β) (G H : Graph α β) :

Prop

Equations

Graph.CompatibleAt e G H = (e ∈ G.edgeSet → e ∈ H.edgeSet → G.IsLink e = H.IsLink e)

Instances For

source

theorem Graph.compatibleAt_def {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} :

CompatibleAt e G H ↔ e ∈ G.edgeSet → e ∈ H.edgeSet → ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y

source

theorem Graph.CompatibleAt.symm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} (h : CompatibleAt e G H) :

CompatibleAt e H G

source

theorem Graph.CompatibleAt.comm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} :

CompatibleAt e G H ↔ CompatibleAt e H G

source

theorem Graph.compatibleAt_self {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G : Graph α β} :

CompatibleAt e G G

source

instance Graph.instIsReflCompatibleAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} :

IsRefl (Graph α β) (CompatibleAt e)

source

instance Graph.instIsSymmCompatibleAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} :

IsSymm (Graph α β) (CompatibleAt e)

source

theorem Graph.compatibleAt_symmetric {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} :

Symmetric (CompatibleAt e)

source

theorem Graph.CompatibleAt.isLink_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} {G H : Graph α β} (h : CompatibleAt e G H) (heG : e ∈ G.edgeSet) (heH : e ∈ H.edgeSet) :

G.IsLink e x y ↔ H.IsLink e x y

source

theorem Graph.compatibleAt_of_notMem_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} (he : e ∉ G.edgeSet) :

CompatibleAt e G H

source

theorem Graph.compatibleAt_of_notMem_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} (he : e ∉ H.edgeSet) :

CompatibleAt e G H

source

theorem Graph.IsLink.compatibleAt_iff_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} {G H : Graph α β} (hIsLink : G.IsLink e x y) :

CompatibleAt e G H ↔ e ∈ H.edgeSet → H.IsLink e x y

source

theorem Graph.IsLink.compatibleAt_iff_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} {G H : Graph α β} (h : H.IsLink e x y) :

CompatibleAt e G H ↔ e ∈ G.edgeSet → G.IsLink e x y

source

theorem Graph.IsLink.of_compatibleAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} {G H : Graph α β} (he : G.IsLink e x y) (h : CompatibleAt e G H) (heH : e ∈ H.edgeSet) :

H.IsLink e x y

source

theorem Graph.CompatibleAt.mono_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H G₀ : Graph α β} (h : CompatibleAt e G H) (hle : G₀ ≤ G) :

CompatibleAt e G₀ H

source

theorem Graph.CompatibleAt.mono_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H H₀ : Graph α β} (h : CompatibleAt e G H) (hH₀ : H₀ ≤ H) :

CompatibleAt e G H₀

source

theorem Graph.CompatibleAt.mono {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H G₀ H₀ : Graph α β} (h : CompatibleAt e G H) (hG : G₀ ≤ G) (hH : H₀ ≤ H) :

CompatibleAt e G₀ H₀

source

theorem Graph.CompatibleAt.induce_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} (h : CompatibleAt e G H) (X : Set α) :

CompatibleAt e G[X] H

source

theorem Graph.CompatibleAt.induce_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} (h : CompatibleAt e G H) (X : Set α) :

CompatibleAt e G H[X]

source

theorem Graph.CompatibleAt.induce {α : Type u_1} {β : Type u_2} [CompleteLattice α] {e : β} {G H : Graph α β} (h : CompatibleAt e G H) (X : Set α) :

CompatibleAt e G[X] H[X]

source

def Graph.Compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G H : Graph α β) :

Prop

Two graphs are Compatible if the edges in their intersection agree on their ends

Equations

G.Compatible H = Set.EqOn G.IsLink H.IsLink (G.edgeSet ∩ H.edgeSet)

Instances For

source

theorem Graph.Compatible.compatibleAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) (e : β) :

CompatibleAt e G H

source

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

G.IsLink e = H.IsLink e

source

theorem Graph.Compatible.symm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) :

H.Compatible G

source

instance Graph.instIsSymmCompatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

IsSymm (Graph α β) Compatible

source

@[simp]

theorem Graph.compatible_symmetric {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

Symmetric Compatible

source

theorem Graph.compatible_comm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} :

G.Compatible H ↔ H.Compatible G

source

theorem Graph.compatible_of_le_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) :

H₁.Compatible H₂

Two subgraphs of the same graph are compatible.

source

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

Pairwise (Function.onFun Compatible Gι)

source

theorem Graph.compatible_of_forall_mem_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} {s : Set (Graph α β)} (h : ∀ ⦃H : Graph α β⦄, H ∈ s → H ≤ G) :

s.Pairwise Compatible

source

theorem Graph.compatible_of_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : H ≤ G) :

H.Compatible G

source

theorem Graph.IsLink.of_compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} {G H : Graph α β} (h : G.IsLink e x y) (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) :

H.IsLink e x y

source

theorem Graph.Inc.of_compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {e : β} {G H : Graph α β} (h : G.Inc e x) (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) :

H.Inc e x

source

theorem Graph.IsLoopAt.of_compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {e : β} {G H : Graph α β} (h : G.IsLoopAt e x) (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) :

H.IsLoopAt e x

source

theorem Graph.IsNonloopAt.of_compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {e : β} {G H : Graph α β} (h : G.IsNonloopAt e x) (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) :

H.IsNonloopAt e x

source

@[simp]

theorem Graph.compatible_self {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G : Graph α β) :

G.Compatible G

source

instance Graph.instIsReflCompatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

IsRefl (Graph α β) Compatible

source

theorem Graph.Compatible.of_disjoint_edgeSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : Disjoint G.edgeSet H.edgeSet) :

G.Compatible H

source

@[simp]

theorem Graph.compatible_edgeDelete_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} :

G.Compatible (H.edgeDelete G.edgeSet)

source

theorem Graph.Compatible.pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) :

{G, H}.Pairwise Compatible

source

@[simp]

theorem Graph.pairwise_compatible_edgeDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} :

{G, H.edgeDelete G.edgeSet}.Pairwise Compatible

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

source

theorem Graph.Compatible.mono_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H G₀ : Graph α β} (h : G.Compatible H) (hG₀ : G₀ ≤ G) :

G₀.Compatible H

source

theorem Graph.Compatible.mono_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H H₀ : Graph α β} (h : G.Compatible H) (hH₀ : H₀ ≤ H) :

G.Compatible H₀

source

theorem Graph.Compatible.mono {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H G₀ H₀ : Graph α β} (h : G.Compatible H) (hG : G₀ ≤ G) (hH : H₀ ≤ H) :

G₀.Compatible H₀

source

theorem Graph.Compatible.induce_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) (X : Set α) :

G[X].Compatible H

source

theorem Graph.Compatible.induce_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) (X : Set α) :

G.Compatible H[X]

source

theorem Graph.Compatible.induce {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} {X : Set α} (h : G.Compatible H) :

G[X].Compatible H[X]

source

theorem Graph.Compatible.vertexDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} {X : Set α} (h : G.Compatible H) :

(G - X).Compatible H - X

source

theorem Graph.Compatible.edgeDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} {F : Set β} (h : G.Compatible H) :

(G.edgeDelete F).Compatible (H.edgeDelete F)

source

theorem Graph.Compatible.edgeRestrict {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} {F : Set β} (h : G.Compatible H) :

(G.edgeRestrict F).Compatible (H.edgeRestrict F)

source

@[simp]

theorem Graph.Compatible.induce_induce {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} {X Y : Set α} :

G[X].Compatible G[Y]

source

theorem Graph.Compatible.stronglyDisjoint_of_vertexSet_disjoint {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) (hV : Disjoint G.vertexSet H.vertexSet) :

G.StronglyDisjoint H

source

theorem Graph.Compatible.disjoint_iff_vertexSet_disjoint {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) :

G.StronglyDisjoint H ↔ Disjoint G.vertexSet H.vertexSet

source

theorem Graph.StronglyDisjoint.compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.StronglyDisjoint H) :

G.Compatible H

source

theorem Graph.Compatible.edgeSet_disjoint_of_vertexSet_disjoint {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Compatible H) (hV : Disjoint G.vertexSet H.vertexSet) :

Disjoint G.edgeSet H.edgeSet

source

theorem Graph.stronglyDisjoint_iff_vertexSet_disjoint_compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} :

G.StronglyDisjoint H ↔ Disjoint G.vertexSet H.vertexSet ∧ G.Compatible H

source

@[deprecated "Pairwise.const_of_refl" (since := "2025-07-30")]

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

Pairwise (Function.onFun Compatible fun (x : ι) => G)

source

@[deprecated "Pairwise.onFun_comp_of_refl" (since := "2025-07-30")]

theorem Graph.pairwise_compatible_comp {α : Type u_1} {β : Type u_2} [CompleteLattice α] {ι : Type u_5} {ι' : Type u_6} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Compatible G)) (f : ι' → ι) :

Pairwise (Function.onFun Compatible (G ∘ f))

source

@[simp]

theorem Graph.stronglyDisjoint_le_compatible {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

StronglyDisjoint ≤ Compatible

useful with Pairwise and Set.Pairwise.

source

def Graph.Dup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G H : Graph α β) :

Prop

Equations

G.Dup_agree H = Function.onFun Partition.Agree Graph.vertexPartition G H

Instances For

source

theorem Graph.Dup_agree.mem_iff_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {G H : Graph α β} (h : G.Dup_agree H) (hxG : x ∈ G.vertexSet) :

x ∈ H.vertexSet ↔ ¬Disjoint H.vertexPartition.supp x

source

@[simp]

theorem Graph.dup_agree_rfl {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} :

G.Dup_agree G

source

instance Graph.instIsReflDup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

IsRefl (Graph α β) Dup_agree

source

theorem Graph.Dup_agree.symm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Dup_agree H) :

H.Dup_agree G

source

instance Graph.instIsSymmDup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

IsSymm (Graph α β) Dup_agree

source

@[simp]

theorem Graph.dup_agree_symmetric {α : Type u_1} {β : Type u_2} [CompleteLattice α] :

Symmetric Dup_agree

source

theorem Graph.Dup_agree_comm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} :

G.Dup_agree H ↔ H.Dup_agree G

source

@[deprecated "Pairwise.onFun_comp_of_refl" (since := "2025-07-30")]

theorem Graph.pairwise_dup_agree_comp {α : Type u_1} {β : Type u_2} [CompleteLattice α] {ι : Type u_5} {ι' : Type u_6} {G : ι → Graph α β} (hG : Pairwise (Function.onFun Dup_agree G)) (f : ι' → ι) :

Pairwise (Function.onFun Dup_agree (G ∘ f))

source

theorem Graph.Dup_agree.mono_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H G₀ : Graph α β} (h : G.Dup_agree H) (hG₀ : G₀ ≤ G) :

G₀.Dup_agree H

source

theorem Graph.Dup_agree.mono_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H H₀ : Graph α β} (h : G.Dup_agree H) (hH₀ : H₀ ≤ H) :

G.Dup_agree H₀

source

theorem Graph.Dup_agree.mono {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H G₀ H₀ : Graph α β} (h : G.Dup_agree H) (hG : G₀ ≤ G) (hH : H₀ ≤ H) :

G₀.Dup_agree H₀

source

theorem Graph.dup_agree_of_le_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) :

H₁.Dup_agree H₂

source

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

Pairwise (Function.onFun Dup_agree Gι)

source

theorem Graph.dup_agree_of_forall_mem_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} {s : Set (Graph α β)} (h : ∀ ⦃H : Graph α β⦄, H ∈ s → H ≤ G) :

s.Pairwise Dup_agree

source

theorem Graph.dup_agree_of_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : H ≤ G) :

H.Dup_agree G

source

theorem Graph.Dup_agree.pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Dup_agree H) :

{G, H}.Pairwise Dup_agree

source

theorem Graph.Dup_agree.pair_edgeDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (h : G.Dup_agree H) :

{G, H.edgeDelete G.edgeSet}.Pairwise Dup_agree

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

source

@[simp]

theorem Graph.Dup_agree.induce {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (X : Set α) (h : G.Dup_agree H) :

G[X].Dup_agree H[X]

source

theorem Graph.Dup_agree.vertexDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (X : Set α) (h : G.Dup_agree H) :

(G - X).Dup_agree H - X

source

theorem Graph.Dup_agree.edgeDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (F : Set β) (h : G.Dup_agree H) :

(G.edgeDelete F).Dup_agree (H.edgeDelete F)

source

theorem Graph.Dup_agree.edgeRestrict {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (F : Set β) (h : G.Dup_agree H) :

(G.edgeRestrict F).Dup_agree (H.edgeRestrict F)

source

theorem Graph.pairwise_dup_agree_eq_pairwise_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {S : Set (Graph α β)} :

S.Pairwise Dup_agree ↔ (vertexPartition '' S).Pairwise Partition.Agree

source

@[simp]

theorem Graph.pairwise_dup_agree_edgeDelete {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G H : Graph α β} (hG' : G.Dup_agree H) :

{G, H.edgeDelete G.edgeSet}.Pairwise Dup_agree

source

theorem Graph.Pairwise.induce_dup_agree {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice α] {G : ι → Graph α β} (h : Pairwise (Function.onFun Dup_agree G)) (P : Set α) :

Pairwise (Function.onFun Dup_agree fun (i : ι) => (G i)[P])

source

theorem Graph.Pairwise.vertexDelete_dup_agree {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice α] {G : ι → Graph α β} (h : Pairwise (Function.onFun Dup_agree G)) (X : Set α) :

Pairwise (Function.onFun Dup_agree fun (i : ι) => (G i) - X)

source

theorem Graph.Pairwise.edgeDelete_dup_agree {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice α] {G : ι → Graph α β} (h : Pairwise (Function.onFun Dup_agree G)) (F : Set β) :

Pairwise (Function.onFun Dup_agree fun (i : ι) => (G i).edgeDelete F)

source

theorem Graph.Pairwise.edgeRestrict_dup_agree {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice α] {G : ι → Graph α β} (h : Pairwise (Function.onFun Dup_agree G)) (F : Set β) :

Pairwise (Function.onFun Dup_agree fun (i : ι) => (G i).edgeRestrict F)

source

theorem Graph.Set.Pairwise.induce_dup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] {S : Set (Graph α β)} (h : S.Pairwise Dup_agree) (P : Set α) :

((fun (x : Graph α β) => x[P]) '' S).Pairwise Dup_agree

source

theorem Graph.Set.Pairwise.vertexDelete_dup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] {S : Set (Graph α β)} (h : S.Pairwise Dup_agree) (X : Set α) :

((fun (x : Graph α β) => x - X) '' S).Pairwise Dup_agree

source

theorem Graph.Set.Pairwise.edgeDelete_dup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] {S : Set (Graph α β)} (h : S.Pairwise Dup_agree) (F : Set β) :

((fun (x : Graph α β) => x.edgeDelete F) '' S).Pairwise Dup_agree

source

theorem Graph.Set.Pairwise.edgeRestrict_dup_agree {α : Type u_1} {β : Type u_2} [CompleteLattice α] {S : Set (Graph α β)} (h : S.Pairwise Dup_agree) (F : Set β) :

((fun (x : Graph α β) => x.edgeRestrict F) '' S).Pairwise Dup_agree