From 9e603d919443d42d94f0e2b976a95a9a906bf201 Mon Sep 17 00:00:00 2001 From: Jun2M Date: Fri, 3 Apr 2026 13:52:30 -0400 Subject: [PATCH 1/6] init --- Mathlib/Combinatorics/Graph/Subgraph.lean | 46 ++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Graph/Subgraph.lean b/Mathlib/Combinatorics/Graph/Subgraph.lean index 2ee8532962d54d..f6868af0b1c27a 100644 --- a/Mathlib/Combinatorics/Graph/Subgraph.lean +++ b/Mathlib/Combinatorics/Graph/Subgraph.lean @@ -13,7 +13,7 @@ public import Mathlib.Tactic.TFAE This file develops the basic theory of subgraphs for multigraphs `Graph α β`: the subgraph relation, standard classes of subgraphs (spanning, induced, closed), -and components. +and the bottom element `⊥`. ## Main definitions @@ -22,6 +22,7 @@ and components. - `H ≤s G` (`Graph.IsSpanningSubgraph`): `H` has the same vertex set as `G`. - `H ≤i G` (`Graph.IsInducedSubgraph`): `H` contains every ambient link between its vertices. - `H ≤c G` (`Graph.IsClosedSubgraph`): `H` is a union of components of `G`. +- `⊥`: empty graph with no vertices or edges as its bottom element. ## Implementation notes @@ -296,6 +297,8 @@ scoped infixl:50 " ≤c " => Graph.IsClosedSubgraph namespace IsClosedSubgraph +alias isInducedSubgraph := toIsInducedSubgraph + lemma mk' (hHG : H ≤ G) (hclosed : ∀ ⦃e x⦄, G.Inc e x → x ∈ V(H) → e ∈ E(H)) : H ≤c G where toIsSubgraph := hHG isLink_of_mem_mem _ _ _ he hx _ := he.anti_of_mem hHG (hclosed he.inc_left hx) @@ -356,4 +359,45 @@ lemma IsInducedSubgraph.not_isClosedSubgraph_iff_exists_isLink (hHG : H ≤i G) end ClosedSubgraph +section OrderBot + +instance : OrderBot (Graph α β) where + bot := noEdge ∅ β + bot_le G := by constructor <;> simp + +instance : Inhabited (Graph α β) where + default := ⊥ + +@[simp] lemma noEdge_empty : Graph.noEdge (∅ : Set α) β = ⊥ := rfl + +@[simp] lemma bot_vertexSet : V((⊥ : Graph α β)) = ∅ := rfl + +@[simp] lemma bot_edgeSet : E((⊥ : Graph α β)) = ∅ := rfl + +@[simp] lemma bot_isClosedSubgraph (G : Graph α β) : ⊥ ≤c G := IsClosedSubgraph.mk' bot_le (by simp) + +@[simp] lemma bot_not_isLink : ¬ (⊥ : Graph α β).IsLink e x y := id + +lemma eq_bot_or_vertexSet_nonempty (G : Graph α β) : G = ⊥ ∨ V(G).Nonempty := by + refine (em (V(G) = ∅)).elim (fun he ↦ .inl (Graph.ext he fun e x y ↦ ?_)) (Or.inr ∘ + nonempty_iff_ne_empty.mpr) + simp only [bot_not_isLink, iff_false] + exact fun h ↦ by simpa [he] using h.left_mem + +@[simp] +lemma vertexSet_eq_empty_iff : V(G) = ∅ ↔ G = ⊥ := by + refine ⟨fun h ↦ bot_le.antisymm' ⟨by simp [h], fun e x y he ↦ ?_⟩, fun h ↦ by simp [h]⟩ + simpa [h] using he.left_mem + +@[push, simp] +lemma ne_bot_iff : G ≠ ⊥ ↔ V(G).Nonempty := not_iff_not.mp <| by simp [not_nonempty_iff_eq_empty] + +@[push, simp] +lemma vertexSet_not_nonempty_iff : ¬ V(G).Nonempty ↔ G = ⊥ := by + simp [not_nonempty_iff_eq_empty] + +lemma ne_bot_of_mem_vertexSet (h : x ∈ V(G)) : G ≠ ⊥ := ne_bot_iff.mpr ⟨x, h⟩ + +end OrderBot + end Graph From 378bfd609e6c027490fba3a3eef86b62d69b2fc6 Mon Sep 17 00:00:00 2001 From: Jun2M Date: Fri, 3 Apr 2026 14:40:13 -0400 Subject: [PATCH 2/6] isClosedSubgraph_bot_iff --- Mathlib/Combinatorics/Graph/Subgraph.lean | 33 +++++++++++++++-------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/Mathlib/Combinatorics/Graph/Subgraph.lean b/Mathlib/Combinatorics/Graph/Subgraph.lean index f6868af0b1c27a..673b0cab66f67c 100644 --- a/Mathlib/Combinatorics/Graph/Subgraph.lean +++ b/Mathlib/Combinatorics/Graph/Subgraph.lean @@ -110,9 +110,9 @@ lemma IsSubgraph.isLink_eqOn (hHG : H ≤ G) : EqOn H.IsLink G.IsLink E(H) := by lemma Compatible.of_le_le (hH₁G : H₁ ≤ G) (hH₂G : H₂ ≤ G) : H₁.Compatible H₂ := fun _ he₁ he₂ _ _ ↦ hH₁G.isLink_iff he₁ |>.trans <| (hH₂G.isLink_iff he₂).symm -lemma Compatible.of_le (hHG : H ≤ G) : H.Compatible G := .of_le_le hHG le_rfl +lemma IsSubgraph.compatible (hHG : H ≤ G) : H.Compatible G := .of_le_le hHG le_rfl -lemma Compatible.of_ge (hHG : G ≤ H) : H.Compatible G := .of_le_le le_rfl hHG +lemma IsSubgraph.compatible' (hHG : G ≤ H) : H.Compatible G := .of_le_le le_rfl hHG lemma Compatible.anti_left (hG₁G : G₁ ≤ G) (h : Compatible G H) : Compatible G₁ H := fun _ he₁ he₂ _ _ ↦ hG₁G.isLink_iff he₁ |>.trans <| h (hG₁G.edgeSet_mono he₁) he₂ .. @@ -166,7 +166,7 @@ lemma Adj.mono (hHG : H ≤ G) (h : H.Adj x y) : G.Adj x y := (h.choose_spec.mono hHG).adj lemma le_iff_compatible_subset_subset : G ≤ H ↔ Compatible G H ∧ V(G) ⊆ V(H) ∧ E(G) ⊆ E(H) := - ⟨fun h ↦ ⟨Compatible.of_le h, h.1, h.edgeSet_mono⟩, fun ⟨h, hV, hE⟩ ↦ + ⟨fun h ↦ ⟨h.compatible, h.1, h.edgeSet_mono⟩, fun ⟨h, hV, hE⟩ ↦ ⟨hV, fun _ _ _ hxy ↦ h hxy.edge_mem (hE hxy.edge_mem) .. |>.mp hxy⟩⟩ lemma Compatible.le_iff (hH : Compatible H₁ H₂) : H₁ ≤ H₂ ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) := @@ -218,7 +218,7 @@ lemma mono_left (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤s G) : K ≤s G where vertexSet_eq := hKG.vertexSet_mono.antisymm <| h.vertexSet_eq.symm.le.trans hHK.vertexSet_mono lemma ext_of_edgeSet (hE : E(H) = E(G)) (h : H ≤s G) : H = G := - (Compatible.of_le h.le).ext h.vertexSet_eq hE + h.compatible.ext h.vertexSet_eq hE end IsSpanningSubgraph @@ -269,7 +269,7 @@ lemma le_of_le_subset (h' : K ≤ G) (hsu : V(K) ⊆ V(H)) (h : H ≤i G) : K exact h.2 (huv.mono h') (hsu huv.left_mem) (hsu huv.right_mem) |>.edge_mem lemma ext_of_vertexSet (hV : V(H) = V(G)) (h : H ≤i G) : H = G := - (Compatible.of_le h.le).ext hV <| antisymm h.edgeSet_mono <| fun e he ↦ by + h.compatible.ext hV <| antisymm h.edgeSet_mono <| fun e he ↦ by obtain ⟨_, _, hxy⟩ := G.exists_isLink_of_mem_edgeSet he exact h.isLink_of_mem_mem hxy (hV ▸ hxy.left_mem) (hV ▸ hxy.right_mem) |>.edge_mem @@ -305,7 +305,7 @@ lemma mk' (hHG : H ≤ G) (hclosed : ∀ ⦃e x⦄, G.Inc e x → x ∈ V(H) → closed _ _ he hx := hclosed he hx protected lemma trans (h₁ : G ≤c G₁) (h₂ : G₁ ≤c G₂) : G ≤c G₂ := - mk' (h₁.le.trans h₂.le) fun _ _ h hx ↦ h₁.closed (h.of_compatible (Compatible.of_ge h₂.le) + mk' (h₁.le.trans h₂.le) fun _ _ h hx ↦ h₁.closed (h.of_compatible h₂.compatible' (h₂.closed h (h₁.vertexSet_mono hx))) hx instance : IsPartialOrder (Graph α β) (· ≤c ·) where @@ -316,7 +316,7 @@ instance : IsPartialOrder (Graph α β) (· ≤c ·) where @[simp] protected lemma rfl : G ≤c G := refl G lemma inc_congr (hx : x ∈ V(H)) (hHG : H ≤c G) : H.Inc e x ↔ G.Inc e x := - ⟨(·.mono hHG.le), fun he ↦ he.of_compatible (Compatible.of_ge hHG.le) (hHG.closed he hx)⟩ + ⟨(·.mono hHG.le), fun he ↦ he.of_compatible hHG.compatible' (hHG.closed he hx)⟩ lemma isLink_congr (hx : x ∈ V(H)) (hHG : H ≤c G) : H.IsLink e x y ↔ G.IsLink e x y := ⟨(·.mono hHG.le), fun h ↦ h.anti_of_mem hHG.le ((hHG.inc_congr hx).mpr h.inc_left).edge_mem⟩ @@ -368,7 +368,7 @@ instance : OrderBot (Graph α β) where instance : Inhabited (Graph α β) where default := ⊥ -@[simp] lemma noEdge_empty : Graph.noEdge (∅ : Set α) β = ⊥ := rfl +@[simp, grind =] lemma noEdge_empty : Graph.noEdge (∅ : Set α) β = ⊥ := rfl @[simp] lemma bot_vertexSet : V((⊥ : Graph α β)) = ∅ := rfl @@ -376,12 +376,11 @@ instance : Inhabited (Graph α β) where @[simp] lemma bot_isClosedSubgraph (G : Graph α β) : ⊥ ≤c G := IsClosedSubgraph.mk' bot_le (by simp) -@[simp] lemma bot_not_isLink : ¬ (⊥ : Graph α β).IsLink e x y := id - lemma eq_bot_or_vertexSet_nonempty (G : Graph α β) : G = ⊥ ∨ V(G).Nonempty := by refine (em (V(G) = ∅)).elim (fun he ↦ .inl (Graph.ext he fun e x y ↦ ?_)) (Or.inr ∘ nonempty_iff_ne_empty.mpr) - simp only [bot_not_isLink, iff_false] + simp only [bot_edgeSet, mem_empty_iff_false, not_false_eq_true, not_isLink_of_notMem_edgeSet, + iff_false] exact fun h ↦ by simpa [he] using h.left_mem @[simp] @@ -398,6 +397,18 @@ lemma vertexSet_not_nonempty_iff : ¬ V(G).Nonempty ↔ G = ⊥ := by lemma ne_bot_of_mem_vertexSet (h : x ∈ V(G)) : G ≠ ⊥ := ne_bot_iff.mpr ⟨x, h⟩ +@[simp] +lemma isSpanningSubgraph_bot_iff : G ≤s ⊥ ↔ G = ⊥ := + ⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩ + +@[simp] +lemma isInducedSubgraph_bot_iff : G ≤i ⊥ ↔ G = ⊥ := + ⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩ + +@[simp] +lemma isClosedSubgraph_bot_iff : G ≤c ⊥ ↔ G = ⊥ := + ⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩ + end OrderBot end Graph From cad5d4000e702dcbd18199f0525300f89dac2728 Mon Sep 17 00:00:00 2001 From: Jun2M Date: Fri, 3 Apr 2026 15:24:11 -0400 Subject: [PATCH 3/6] disjoint --- Mathlib/Combinatorics/Graph/Subgraph.lean | 27 +++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/Mathlib/Combinatorics/Graph/Subgraph.lean b/Mathlib/Combinatorics/Graph/Subgraph.lean index 673b0cab66f67c..ac6299a092e4ca 100644 --- a/Mathlib/Combinatorics/Graph/Subgraph.lean +++ b/Mathlib/Combinatorics/Graph/Subgraph.lean @@ -181,6 +181,14 @@ lemma vertexSet_ssubset_or_edgeSet_ssubset_of_lt (hGH : G < H) : V(G) ⊂ V(H) by_contra! heq exact hGH.2 <| (Compatible.of_le_le hGH.1 le_rfl).ext heq.1 heq.2 +@[simp] +lemma noEdge_le_iff : noEdge X β ≤ G ↔ X ⊆ V(G) := ⟨(·.vertexSet_mono), fun h ↦ ⟨h, by simp⟩⟩ + +@[simp] +lemma le_noEdge_iff : G ≤ noEdge X β ↔ V(G) ⊆ X ∧ E(G) = ∅ := + ⟨fun h ↦ ⟨h.vertexSet_mono, subset_empty_iff.1 h.edgeSet_mono⟩, + fun h ↦ ⟨h.1, fun e x y he ↦ by simpa [h] using he.edge_mem⟩⟩ + end Subgraph section SpanningSubgraph @@ -220,6 +228,14 @@ lemma mono_left (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤s G) : K ≤s G where lemma ext_of_edgeSet (hE : E(H) = E(G)) (h : H ≤s G) : H = G := h.compatible.ext h.vertexSet_eq hE +@[gcongr] +lemma bouquet_mono (h : F₁ ⊆ F₂) : bouquet x F₁ ≤s bouquet x F₂ where + vertexSet_eq := rfl + +@[gcongr] +lemma banana_mono (hF : F₁ ⊆ F₂) : banana u v F₁ ≤s banana u v F₂ where + vertexSet_eq := rfl + end IsSpanningSubgraph end SpanningSubgraph @@ -409,6 +425,17 @@ lemma isInducedSubgraph_bot_iff : G ≤i ⊥ ↔ G = ⊥ := lemma isClosedSubgraph_bot_iff : G ≤c ⊥ ↔ G = ⊥ := ⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩ +lemma not_disjoint_of_mem_mem (h : x ∈ V(G)) (h' : x ∈ V(H)) : ¬ Disjoint G H := by + simp only [Disjoint, le_bot_iff, not_forall, ne_eq, ne_bot_iff] + use noEdge {x} β + simp [h, h'] + +lemma vertexSet_disjoint_of_disjoint (h : Disjoint G H) : Disjoint V(G) V(H) := by + contrapose! h + rw [not_disjoint_iff] at h + obtain ⟨x, hx₁, hx₂⟩ := h + exact not_disjoint_of_mem_mem hx₁ hx₂ + end OrderBot end Graph From bddb03240865647ce821508119bf7f5a42f8826d Mon Sep 17 00:00:00 2001 From: Jun2M Date: Wed, 8 Apr 2026 14:58:16 -0400 Subject: [PATCH 4/6] Apply comment --- Mathlib/Combinatorics/Graph/Subgraph.lean | 47 ++++++++++------------- 1 file changed, 20 insertions(+), 27 deletions(-) diff --git a/Mathlib/Combinatorics/Graph/Subgraph.lean b/Mathlib/Combinatorics/Graph/Subgraph.lean index ac6299a092e4ca..0e9c677a95130d 100644 --- a/Mathlib/Combinatorics/Graph/Subgraph.lean +++ b/Mathlib/Combinatorics/Graph/Subgraph.lean @@ -110,9 +110,11 @@ lemma IsSubgraph.isLink_eqOn (hHG : H ≤ G) : EqOn H.IsLink G.IsLink E(H) := by lemma Compatible.of_le_le (hH₁G : H₁ ≤ G) (hH₂G : H₂ ≤ G) : H₁.Compatible H₂ := fun _ he₁ he₂ _ _ ↦ hH₁G.isLink_iff he₁ |>.trans <| (hH₂G.isLink_iff he₂).symm -lemma IsSubgraph.compatible (hHG : H ≤ G) : H.Compatible G := .of_le_le hHG le_rfl +lemma Compatible.of_le (hHG : H ≤ G) : H.Compatible G := .of_le_le hHG le_rfl +alias IsSubgraph.compatible := Compatible.of_le -lemma IsSubgraph.compatible' (hHG : G ≤ H) : H.Compatible G := .of_le_le le_rfl hHG +lemma Compatible.of_ge (hHG : G ≤ H) : H.Compatible G := .of_le_le le_rfl hHG +alias IsSubgraph.compatible' := Compatible.of_ge lemma Compatible.anti_left (hG₁G : G₁ ≤ G) (h : Compatible G H) : Compatible G₁ H := fun _ he₁ he₂ _ _ ↦ hG₁G.isLink_iff he₁ |>.trans <| h (hG₁G.edgeSet_mono he₁) he₂ .. @@ -166,7 +168,7 @@ lemma Adj.mono (hHG : H ≤ G) (h : H.Adj x y) : G.Adj x y := (h.choose_spec.mono hHG).adj lemma le_iff_compatible_subset_subset : G ≤ H ↔ Compatible G H ∧ V(G) ⊆ V(H) ∧ E(G) ⊆ E(H) := - ⟨fun h ↦ ⟨h.compatible, h.1, h.edgeSet_mono⟩, fun ⟨h, hV, hE⟩ ↦ + ⟨fun h ↦ ⟨.of_le h, h.1, h.edgeSet_mono⟩, fun ⟨h, hV, hE⟩ ↦ ⟨hV, fun _ _ _ hxy ↦ h hxy.edge_mem (hE hxy.edge_mem) .. |>.mp hxy⟩⟩ lemma Compatible.le_iff (hH : Compatible H₁ H₂) : H₁ ≤ H₂ ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) := @@ -179,7 +181,7 @@ lemma vertexSet_ssubset_or_edgeSet_ssubset_of_lt (hGH : G < H) : V(G) ⊂ V(H) rw [lt_iff_le_and_ne] at hGH simp only [ssubset_iff_subset_ne, hGH.1.vertexSet_mono, ne_eq, true_and, hGH.1.edgeSet_mono] by_contra! heq - exact hGH.2 <| (Compatible.of_le_le hGH.1 le_rfl).ext heq.1 heq.2 + exact hGH.2 <| hGH.1.compatible.ext heq.1 heq.2 @[simp] lemma noEdge_le_iff : noEdge X β ≤ G ↔ X ⊆ V(G) := ⟨(·.vertexSet_mono), fun h ↦ ⟨h, by simp⟩⟩ @@ -197,7 +199,7 @@ section SpanningSubgraph /-- `H ≤s G` (`Graph.IsSpanningSubgraph`) is a subgraph of `G` with the same vertex set. -/ @[mk_iff] -structure IsSpanningSubgraph (H G : Graph α β) : Prop extends H ≤ G where +structure IsSpanningSubgraph (H G : Graph α β) : Prop extends le : H ≤ G where vertexSet_eq : V(H) = V(G) @[inherit_doc IsSpanningSubgraph] @@ -205,8 +207,6 @@ infixl:50 " ≤s " => Graph.IsSpanningSubgraph namespace IsSpanningSubgraph -protected alias le := toIsSubgraph - protected lemma trans (h₁ : G ≤s G₁) (h₂ : G₁ ≤s G₂) : G ≤s G₂ := ⟨h₁.le.trans h₂.le, h₁.vertexSet_eq.trans h₂.vertexSet_eq⟩ @@ -218,20 +218,16 @@ instance : IsPartialOrder (Graph α β) (· ≤s ·) where @[simp] protected lemma rfl : G ≤s G := refl G lemma anti_right (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤s G) : H ≤s K where - toIsSubgraph := hHK + le := hHK vertexSet_eq := hHK.vertexSet_mono.antisymm <| hKG.vertexSet_mono.trans_eq h.vertexSet_eq.symm lemma mono_left (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤s G) : K ≤s G where - toIsSubgraph := hKG + le := hKG vertexSet_eq := hKG.vertexSet_mono.antisymm <| h.vertexSet_eq.symm.le.trans hHK.vertexSet_mono lemma ext_of_edgeSet (hE : E(H) = E(G)) (h : H ≤s G) : H = G := h.compatible.ext h.vertexSet_eq hE -@[gcongr] -lemma bouquet_mono (h : F₁ ⊆ F₂) : bouquet x F₁ ≤s bouquet x F₂ where - vertexSet_eq := rfl - @[gcongr] lemma banana_mono (hF : F₁ ⊆ F₂) : banana u v F₁ ≤s banana u v F₂ where vertexSet_eq := rfl @@ -247,7 +243,7 @@ section InducedSubgraph /-- `H ≤i G` (`Graph.IsInducedSubgraph`) is a subgraph of `G` such that every link of `G` involving two vertices of `H` is also a link of `H`. -/ @[mk_iff] -structure IsInducedSubgraph (H G : Graph α β) : Prop extends H ≤ G where +structure IsInducedSubgraph (H G : Graph α β) : Prop extends le : H ≤ G where isLink_of_mem_mem : ∀ ⦃e x y⦄, G.IsLink e x y → x ∈ V(H) → y ∈ V(H) → H.IsLink e x y @[inherit_doc IsInducedSubgraph] @@ -255,8 +251,6 @@ scoped infixl:50 " ≤i " => Graph.IsInducedSubgraph namespace IsInducedSubgraph -alias le := toIsSubgraph - protected lemma trans (h₁ : G ≤i G₁) (h₂ : G₁ ≤i G₂) : G ≤i G₂ := ⟨h₁.le.trans h₂.le, fun _ _ _ h hx hy ↦ h₁.isLink_of_mem_mem (h₂.isLink_of_mem_mem h (h₁.vertexSet_mono hx) (h₁.vertexSet_mono hy)) hx hy⟩ @@ -276,7 +270,7 @@ lemma adj_congr (hx : x ∈ V(H)) (hy : y ∈ V(H)) (h : H ≤i G) : H.Adj x y ⟨(·.mono h.le), fun ⟨_, hxy⟩ ↦ (h.isLink_of_mem_mem hxy hx hy).adj⟩ lemma anti_right (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤i G) : H ≤i K where - toIsSubgraph := hHK + le := hHK isLink_of_mem_mem _ _ _ hxy hx hy := h.isLink_of_mem_mem (hxy.mono hKG) hx hy lemma le_of_le_subset (h' : K ≤ G) (hsu : V(K) ⊆ V(H)) (h : H ≤i G) : K ≤ H := by @@ -305,7 +299,8 @@ section ClosedSubgraph /-- `H ≤c G` (`Graph.IsClosedSubgraph`) is a union of components of `G`. -/ @[mk_iff] -structure IsClosedSubgraph (H G : Graph α β) : Prop extends IsInducedSubgraph H G where +structure IsClosedSubgraph (H G : Graph α β) : Prop extends + isInducedSubgraph : IsInducedSubgraph H G where closed : ∀ ⦃e x⦄, G.Inc e x → x ∈ V(H) → e ∈ E(H) @[inherit_doc IsClosedSubgraph] @@ -313,10 +308,8 @@ scoped infixl:50 " ≤c " => Graph.IsClosedSubgraph namespace IsClosedSubgraph -alias isInducedSubgraph := toIsInducedSubgraph - lemma mk' (hHG : H ≤ G) (hclosed : ∀ ⦃e x⦄, G.Inc e x → x ∈ V(H) → e ∈ E(H)) : H ≤c G where - toIsSubgraph := hHG + le := hHG isLink_of_mem_mem _ _ _ he hx _ := he.anti_of_mem hHG (hclosed he.inc_left hx) closed _ _ he hx := hclosed he hx @@ -386,30 +379,30 @@ instance : Inhabited (Graph α β) where @[simp, grind =] lemma noEdge_empty : Graph.noEdge (∅ : Set α) β = ⊥ := rfl -@[simp] lemma bot_vertexSet : V((⊥ : Graph α β)) = ∅ := rfl +@[simp] lemma vertexSet_bot : V((⊥ : Graph α β)) = ∅ := rfl -@[simp] lemma bot_edgeSet : E((⊥ : Graph α β)) = ∅ := rfl +@[simp] lemma edgeSet_bot : E((⊥ : Graph α β)) = ∅ := rfl @[simp] lemma bot_isClosedSubgraph (G : Graph α β) : ⊥ ≤c G := IsClosedSubgraph.mk' bot_le (by simp) lemma eq_bot_or_vertexSet_nonempty (G : Graph α β) : G = ⊥ ∨ V(G).Nonempty := by refine (em (V(G) = ∅)).elim (fun he ↦ .inl (Graph.ext he fun e x y ↦ ?_)) (Or.inr ∘ nonempty_iff_ne_empty.mpr) - simp only [bot_edgeSet, mem_empty_iff_false, not_false_eq_true, not_isLink_of_notMem_edgeSet, + simp only [edgeSet_bot, mem_empty_iff_false, not_false_eq_true, not_isLink_of_notMem_edgeSet, iff_false] exact fun h ↦ by simpa [he] using h.left_mem -@[simp] lemma vertexSet_eq_empty_iff : V(G) = ∅ ↔ G = ⊥ := by refine ⟨fun h ↦ bot_le.antisymm' ⟨by simp [h], fun e x y he ↦ ?_⟩, fun h ↦ by simp [h]⟩ simpa [h] using he.left_mem @[push, simp] -lemma ne_bot_iff : G ≠ ⊥ ↔ V(G).Nonempty := not_iff_not.mp <| by simp [not_nonempty_iff_eq_empty] +lemma ne_bot_iff : G ≠ ⊥ ↔ V(G).Nonempty := + not_iff_not.mp <| by simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty] @[push, simp] lemma vertexSet_not_nonempty_iff : ¬ V(G).Nonempty ↔ G = ⊥ := by - simp [not_nonempty_iff_eq_empty] + simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty] lemma ne_bot_of_mem_vertexSet (h : x ∈ V(G)) : G ≠ ⊥ := ne_bot_iff.mpr ⟨x, h⟩ From c298fd6756adad724c6f8ef174f79b46530a1cbf Mon Sep 17 00:00:00 2001 From: Jun Kwon Date: Thu, 9 Apr 2026 09:14:20 -0400 Subject: [PATCH 5/6] Update Mathlib/Combinatorics/Graph/Subgraph.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Combinatorics/Graph/Subgraph.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/Graph/Subgraph.lean b/Mathlib/Combinatorics/Graph/Subgraph.lean index 0e9c677a95130d..9a3eb06df09747 100644 --- a/Mathlib/Combinatorics/Graph/Subgraph.lean +++ b/Mathlib/Combinatorics/Graph/Subgraph.lean @@ -111,9 +111,9 @@ lemma Compatible.of_le_le (hH₁G : H₁ ≤ G) (hH₂G : H₂ ≤ G) : H₁.Com fun _ he₁ he₂ _ _ ↦ hH₁G.isLink_iff he₁ |>.trans <| (hH₂G.isLink_iff he₂).symm lemma Compatible.of_le (hHG : H ≤ G) : H.Compatible G := .of_le_le hHG le_rfl -alias IsSubgraph.compatible := Compatible.of_le - lemma Compatible.of_ge (hHG : G ≤ H) : H.Compatible G := .of_le_le le_rfl hHG + +alias IsSubgraph.compatible := Compatible.of_le alias IsSubgraph.compatible' := Compatible.of_ge lemma Compatible.anti_left (hG₁G : G₁ ≤ G) (h : Compatible G H) : Compatible G₁ H := From 0b0786d51d2011dca4013a77f8a2a5027f3e04b7 Mon Sep 17 00:00:00 2001 From: Jun2M Date: Thu, 9 Apr 2026 09:15:41 -0400 Subject: [PATCH 6/6] rm vertexSet_disjoint_of_disjoint --- Mathlib/Combinatorics/Graph/Subgraph.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Mathlib/Combinatorics/Graph/Subgraph.lean b/Mathlib/Combinatorics/Graph/Subgraph.lean index 9a3eb06df09747..dd64c9f1e464fd 100644 --- a/Mathlib/Combinatorics/Graph/Subgraph.lean +++ b/Mathlib/Combinatorics/Graph/Subgraph.lean @@ -423,12 +423,6 @@ lemma not_disjoint_of_mem_mem (h : x ∈ V(G)) (h' : x ∈ V(H)) : ¬ Disjoint G use noEdge {x} β simp [h, h'] -lemma vertexSet_disjoint_of_disjoint (h : Disjoint G H) : Disjoint V(G) V(H) := by - contrapose! h - rw [not_disjoint_iff] at h - obtain ⟨x, hx₁, hx₂⟩ := h - exact not_disjoint_of_mem_mem hx₁ hx₂ - end OrderBot end Graph