@[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 instReflOnFun_matroid {α : Type u_1} {ι : Type u_5} {r : α → α → Prop} [Std.Refl r] {f : ι → α} : Std.Refl (Function.onFun r f)

Compatibility

@[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.Compatible.pair {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : {G, H}.Pairwise Compatible

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.deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} {X : Set α} (h : G.Compatible H) : (G.deleteVerts X).Compatible (H.deleteVerts X)

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

theorem Graph.Compatible.restrict {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (h : G.Compatible H) : (G.restrict F).Compatible (H.restrict 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.