@[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

instance instIsReflOnFun_matroid {ι : Type u_5} {α : Type u_6} {r : α → α → Prop} [IsRefl α r] {f : ι → α} : IsRefl ι (Function.onFun r f)

Strongly disjointness

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

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.StronglyDisjoint.disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.StronglyDisjoint H) : Disjoint G H

Compatibility

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

Equations

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

theorem Graph.compatibleAt_def {α : Type u_1} {β : Type u_2} {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

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

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

theorem Graph.compatibleAt_self {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} : CompatibleAt e G G

instance Graph.instIsReflCompatibleAt {α : Type u_1} {β : Type u_2} {e : β} : IsRefl (Graph α β) (CompatibleAt e)

instance Graph.instIsSymmCompatibleAt {α : Type u_1} {β : Type u_2} {e : β} : IsSymm (Graph α β) (CompatibleAt e)

theorem Graph.compatibleAt_symmetric {α : Type u_1} {β : Type u_2} {e : β} : Symmetric (CompatibleAt e)

theorem Graph.CompatibleAt.isLink_iff {α : Type u_1} {β : Type u_2} {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

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

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

theorem Graph.IsLink.compatibleAt_iff_left {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hIsLink : G.IsLink e x y) : CompatibleAt e G H ↔ e ∈ H.edgeSet → H.IsLink e x y

theorem Graph.IsLink.compatibleAt_iff_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (h : H.IsLink e x y) : CompatibleAt e G H ↔ e ∈ G.edgeSet → G.IsLink e x y

theorem Graph.IsLink.of_compatibleAt {α : Type u_1} {β : Type u_2} {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

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

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

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

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

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

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

def Graph.Compatible {α : Type u_1} {β : Type u_2} (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)

@[simp]

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

@[simp]

theorem Graph.pairwise_compatibleAt_of_compatible {α : Type u_1} {β : Type u_2} {ι : Type u_3} {Gι : ι → Graph α β} (h : Pairwise (Function.onFun Compatible Gι)) (e : β) : Pairwise (Function.onFun (CompatibleAt e) Gι)

@[simp]

theorem Graph.set_pairwise_compatibleAt_of_compatible {α : Type u_1} {β : Type u_2} {s : Set (Graph α β)} (h : s.Pairwise Compatible) (e : β) : s.Pairwise (CompatibleAt e)

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

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

instance Graph.instIsSymmCompatible {α : Type u_1} {β : Type u_2} : IsSymm (Graph α β) Compatible

@[simp]

theorem Graph.compatible_symmetric {α : Type u_1} {β : Type u_2} : Symmetric Compatible

theorem Graph.compatible_comm {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G.Compatible H ↔ H.Compatible G

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

Two subgraphs of the same graph are compatible.

theorem Graph.compatible_of_forall_map_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {Gι : ι → Graph α β} (h : ∀ (i : ι), Gι i ≤ G) : Pairwise (Function.onFun Compatible Gι)

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

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

theorem Graph.IsLink.of_compatible {α : Type u_1} {β : Type u_2} {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

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

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

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

@[simp]

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

instance Graph.instIsReflCompatible {α : Type u_1} {β : Type u_2} : IsRefl (Graph α β) Compatible

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

theorem Graph.Compatible.disjoint_iff_vertexSet_disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : G.StronglyDisjoint H ↔ Disjoint G.vertexSet H.vertexSet

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

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

theorem Graph.stronglyDisjoint_iff_vertexSet_disjoint_compatible {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G.StronglyDisjoint H ↔ Disjoint G.vertexSet H.vertexSet ∧ G.Compatible H

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

theorem Graph.pairwise_compatible_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} (G : Graph α β) : Pairwise (Function.onFun Compatible fun (x : ι) => G)

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

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

@[simp]

theorem Graph.stronglyDisjoint_le_compatible {α : Type u_1} {β : Type u_2} : StronglyDisjoint ≤ Compatible

useful with Pairwise and Set.Pairwise.