From 4c562deb5dde60528bcd95d1394fed40af0fbcc1 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 6 Aug 2026 13:27:45 +0300 Subject: [PATCH 01/63] feat(Combinatorics/SimpleGraph/Connectivity): add edge reachability and connectivity numbers --- .../Combinatorics/SimpleGraph/AdjMatrix.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 4 ++- .../Connectivity/EdgeConnectivity.lean | 35 +++++++++++++++++++ Mathlib/Data/ENat/Basic.lean | 6 ++-- Mathlib/Data/ENat/Defs.lean | 4 ++- scripts/i_am_a_file_name_with_no_clashes | 0 6 files changed, 46 insertions(+), 5 deletions(-) create mode 100644 scripts/i_am_a_file_name_with_no_clashes diff --git a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean index e3f9ae59fd486b..c96bc8144bce92 100644 --- a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean @@ -250,7 +250,7 @@ theorem adjMatrix_bot [Zero α] [One α] : ext; simp @[simp] -theorem adjMatrix_top [DecidableEq V] [Ring α] : +theorem adjMatrix_top [DecidableEq V] [Zero α] [One α] : (⊤ : SimpleGraph V).adjMatrix α = .of (fun i j ↦ if i = j then 0 else 1) := by ext i j cases eq_or_ne i j <;> simp [‹_›] diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index c2b8107c55eb08..8727e2379f00e6 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -318,7 +318,9 @@ instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGrap isGLB_sInf _ := ⟨fun _ hG _ _ hab ↦ hab.1 hG, fun _ hG _ _ hab ↦ ⟨fun _ hH => hG hH hab, hab.ne⟩⟩ iInf_iSup_eq f := by ext; simp [Classical.skolem] -/-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices. -/ +/-- The complete graph on a type `V` is the simple graph in which every pair +of distinct vertices is adjacent. +-/ @[wikidata Q45715] abbrev completeGraph (V : Type u) : SimpleGraph V := ⊤ diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f0570db48af00b..b9b53275def311 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -7,6 +7,8 @@ module public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected public import Mathlib.Data.Set.Card +public import Mathlib.Order.CompletePartialOrder +public import Mathlib.Data.ENat.Lattice /-! # Edge Connectivity @@ -168,6 +170,39 @@ lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u refine (Set.subsingleton_iff_singleton h').mp ?_ exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs) +noncomputable def edgeReachability (G : SimpleGraph V) (u v : V) : ℕ∞ := + ⨆ (k : ℕ) (_ : G.IsEdgeReachable k u v), k + +noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := + ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k + +theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by + simp only [edgeConnectivity, IsEdgeConnected, IsEdgeReachable, Subsingleton.forall₂_iff, + Reachable.rfl, implies_true, iSup_pos] + exact ENat.iSup_natCast + +theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by + simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] + +theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by + simp only [isEdgeReachable_comm,edgeReachability] + +theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := by + apply iSup_le + intro k + apply iSup_le + intro hk + unfold edgeReachability + apply le_iSup_of_le + apply le_iSup_of_le + exact le_rfl + have := hk u v + assumption +-- exact le_iSup_of_le k <| le_iSup_of_le (hk u v) le_rfl + + + + /-! ### 2-reachability diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean index d7ead409489d53..00ec5a3777081a 100644 --- a/Mathlib/Data/ENat/Basic.lean +++ b/Mathlib/Data/ENat/Basic.lean @@ -17,8 +17,10 @@ public import Mathlib.Data.Nat.SuccPred /-! # Definition and basic properties of extended natural numbers -In this file we define `ENat` (notation: `ℕ∞`) to be `WithTop ℕ` and prove some basic lemmas -about this type. +In this file, we prove some basic lemmas +about `ENat` (notation: `ℕ∞`). + +Refer to `ENat/Defs.lean` for the definition and notation ## Implementation details diff --git a/Mathlib/Data/ENat/Defs.lean b/Mathlib/Data/ENat/Defs.lean index 3558a5153a0b17..14fb9c0fbd4b67 100644 --- a/Mathlib/Data/ENat/Defs.lean +++ b/Mathlib/Data/ENat/Defs.lean @@ -9,7 +9,9 @@ public import Batteries.Tactic.Alias public import Mathlib.Data.Nat.Notation public import Mathlib.Order.TypeTags -/-! # Definition and notation for extended natural numbers -/ +/-! # Definition and notation for extended natural numbers +In this file we define `ENat` (notation: `ℕ∞`) to be `WithTop ℕ` +-/ @[expose] public section diff --git a/scripts/i_am_a_file_name_with_no_clashes b/scripts/i_am_a_file_name_with_no_clashes new file mode 100644 index 00000000000000..e69de29bb2d1d6 From deb56a06c3572129f266a10a3fb079ec120c1445 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Thu, 6 Aug 2026 10:35:54 +0000 Subject: [PATCH 02/63] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 2 +- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- Mathlib/Data/ENat/Basic.lean | 2 +- Mathlib/Data/ENat/Defs.lean | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 8727e2379f00e6..7f706310542c1d 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -318,7 +318,7 @@ instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGrap isGLB_sInf _ := ⟨fun _ hG _ _ hab ↦ hab.1 hG, fun _ hG _ _ hab ↦ ⟨fun _ hH => hG hH hab, hab.ne⟩⟩ iInf_iSup_eq f := by ext; simp [Classical.skolem] -/-- The complete graph on a type `V` is the simple graph in which every pair +/-- The complete graph on a type `V` is the simple graph in which every pair of distinct vertices is adjacent. -/ @[wikidata Q45715] diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index b9b53275def311..c935f59b29978c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -182,7 +182,7 @@ theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnect exact ENat.iSup_natCast theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by - simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] + simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm,edgeReachability] @@ -192,7 +192,7 @@ theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReac intro k apply iSup_le intro hk - unfold edgeReachability + unfold edgeReachability apply le_iSup_of_le apply le_iSup_of_le exact le_rfl diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean index 00ec5a3777081a..e93a5120810dfd 100644 --- a/Mathlib/Data/ENat/Basic.lean +++ b/Mathlib/Data/ENat/Basic.lean @@ -18,7 +18,7 @@ public import Mathlib.Data.Nat.SuccPred # Definition and basic properties of extended natural numbers In this file, we prove some basic lemmas -about `ENat` (notation: `ℕ∞`). +about `ENat` (notation: `ℕ∞`). Refer to `ENat/Defs.lean` for the definition and notation diff --git a/Mathlib/Data/ENat/Defs.lean b/Mathlib/Data/ENat/Defs.lean index 14fb9c0fbd4b67..273b551607a2d8 100644 --- a/Mathlib/Data/ENat/Defs.lean +++ b/Mathlib/Data/ENat/Defs.lean @@ -9,7 +9,7 @@ public import Batteries.Tactic.Alias public import Mathlib.Data.Nat.Notation public import Mathlib.Order.TypeTags -/-! # Definition and notation for extended natural numbers +/-! # Definition and notation for extended natural numbers In this file we define `ENat` (notation: `ℕ∞`) to be `WithTop ℕ` -/ From facdcae17732abb31012900f2427cfca911df5e8 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 6 Aug 2026 13:42:50 +0300 Subject: [PATCH 03/63] remove file from scripts --- scripts/i_am_a_file_name_with_no_clashes | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 scripts/i_am_a_file_name_with_no_clashes diff --git a/scripts/i_am_a_file_name_with_no_clashes b/scripts/i_am_a_file_name_with_no_clashes deleted file mode 100644 index e69de29bb2d1d6..00000000000000 From a4a5e4148573ac9326b0bf5a66494f1864dd5541 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 6 Aug 2026 14:19:34 +0300 Subject: [PATCH 04/63] Ring --- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean index c96bc8144bce92..e3f9ae59fd486b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean @@ -250,7 +250,7 @@ theorem adjMatrix_bot [Zero α] [One α] : ext; simp @[simp] -theorem adjMatrix_top [DecidableEq V] [Zero α] [One α] : +theorem adjMatrix_top [DecidableEq V] [Ring α] : (⊤ : SimpleGraph V).adjMatrix α = .of (fun i j ↦ if i = j then 0 else 1) := by ext i j cases eq_or_ne i j <;> simp [‹_›] From 56d3f93044fbe9d05f28885fad3b628e57bc37d7 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 6 Aug 2026 17:46:24 +0300 Subject: [PATCH 05/63] fix ci --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index c935f59b29978c..178baf160a179c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -194,15 +194,13 @@ theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReac intro hk unfold edgeReachability apply le_iSup_of_le - apply le_iSup_of_le - exact le_rfl - have := hk u v - assumption + · apply le_iSup_of_le + · exact le_rfl + have := hk u v + assumption -- exact le_iSup_of_le k <| le_iSup_of_le (hk u v) le_rfl - - /-! ### 2-reachability From 8aede9b63d3d0c88b6c45a38bcca8d716bedcdff Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 6 Aug 2026 17:56:19 +0300 Subject: [PATCH 06/63] remove docstring changes --- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 4 +--- Mathlib/Data/ENat/Basic.lean | 6 ++---- Mathlib/Data/ENat/Defs.lean | 4 +--- 3 files changed, 4 insertions(+), 10 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 28b30c3f291a6a..8ce12ed2ddcb40 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -318,9 +318,7 @@ instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGrap isGLB_sInf _ := ⟨fun _ hG _ _ hab ↦ hab.1 hG, fun _ hG _ _ hab ↦ ⟨fun _ hH => hG hH hab, hab.ne⟩⟩ iInf_iSup_eq f := by ext; simp [Classical.skolem] -/-- The complete graph on a type `V` is the simple graph in which every pair -of distinct vertices is adjacent. --/ +/-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices. -/ @[wikidata Q45715] abbrev completeGraph (V : Type u) : SimpleGraph V := ⊤ diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean index e93a5120810dfd..d7ead409489d53 100644 --- a/Mathlib/Data/ENat/Basic.lean +++ b/Mathlib/Data/ENat/Basic.lean @@ -17,10 +17,8 @@ public import Mathlib.Data.Nat.SuccPred /-! # Definition and basic properties of extended natural numbers -In this file, we prove some basic lemmas -about `ENat` (notation: `ℕ∞`). - -Refer to `ENat/Defs.lean` for the definition and notation +In this file we define `ENat` (notation: `ℕ∞`) to be `WithTop ℕ` and prove some basic lemmas +about this type. ## Implementation details diff --git a/Mathlib/Data/ENat/Defs.lean b/Mathlib/Data/ENat/Defs.lean index 273b551607a2d8..3558a5153a0b17 100644 --- a/Mathlib/Data/ENat/Defs.lean +++ b/Mathlib/Data/ENat/Defs.lean @@ -9,9 +9,7 @@ public import Batteries.Tactic.Alias public import Mathlib.Data.Nat.Notation public import Mathlib.Order.TypeTags -/-! # Definition and notation for extended natural numbers -In this file we define `ENat` (notation: `ℕ∞`) to be `WithTop ℕ` --/ +/-! # Definition and notation for extended natural numbers -/ @[expose] public section From 78bffa593bfd178eb1bf1f51b241ed98076ff1b8 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Thu, 6 Aug 2026 18:33:07 +0300 Subject: [PATCH 07/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 178baf160a179c..775083a1db6fe5 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -171,7 +171,7 @@ lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs) noncomputable def edgeReachability (G : SimpleGraph V) (u v : V) : ℕ∞ := - ⨆ (k : ℕ) (_ : G.IsEdgeReachable k u v), k + ⨆ (k : ℕ) (_ : G.IsEdgeReachable k u v), k noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k From 87ac82c62af13253630e97f6235bebe7a770f637 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 6 Aug 2026 18:37:07 +0300 Subject: [PATCH 08/63] golfed --- .../Connectivity/EdgeConnectivity.lean | 22 +++++++++---------- 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 178baf160a179c..2b13b21270a42f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -187,18 +187,16 @@ theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm,edgeReachability] -theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := by - apply iSup_le - intro k - apply iSup_le - intro hk - unfold edgeReachability - apply le_iSup_of_le - · apply le_iSup_of_le - · exact le_rfl - have := hk u v - assumption --- exact le_iSup_of_le k <| le_iSup_of_le (hk u v) le_rfl +theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := + iSup_le + fun k ↦ + iSup_le fun hk ↦ + id + (le_iSup_of_le k + (le_iSup_of_le + (have this := hk u v; + this) + le_rfl)) /-! From 4313ee34a080b128ed9bcb064ae113a6c41fd564 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Thu, 6 Aug 2026 15:40:42 +0000 Subject: [PATCH 09/63] [pre-commit.ci lite] apply automatic fixes --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 1f683a282d313f..40f4a132bcc0e1 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -187,7 +187,7 @@ theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm,edgeReachability] -theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := +theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup_le fun k ↦ iSup_le fun hk ↦ From 25576b76fe8ceaa5eb71cafaa47cd08844dd627e Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Fri, 7 Aug 2026 23:22:40 +0300 Subject: [PATCH 10/63] simp suggestion --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 1f683a282d313f..36dfd10d66f48d 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -177,9 +177,7 @@ noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by - simp only [edgeConnectivity, IsEdgeConnected, IsEdgeReachable, Subsingleton.forall₂_iff, - Reachable.rfl, implies_true, iSup_pos] - exact ENat.iSup_natCast + simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] @@ -187,7 +185,7 @@ theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm,edgeReachability] -theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := +theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup_le fun k ↦ iSup_le fun hk ↦ From 7e49347c4b8f3aaea78fb9627615d25cbba19cde Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Fri, 7 Aug 2026 23:32:11 +0300 Subject: [PATCH 11/63] shorter proof --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 36dfd10d66f48d..9f866ec11c200c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -186,15 +186,10 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u simp only [isEdgeReachable_comm,edgeReachability] theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := - iSup_le - fun k ↦ - iSup_le fun hk ↦ - id - (le_iSup_of_le k - (le_iSup_of_le - (have this := hk u v; - this) - le_rfl)) + iSup₂_le ( + fun i hi ↦ + le_iSup₂_of_le i (hi u v) le_rfl + ) /-! From 19af63a661a13a1a5284d10f66be9944dd2dd891 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Fri, 7 Aug 2026 23:34:06 +0300 Subject: [PATCH 12/63] fixed spacing --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 9f866ec11c200c..c269b9af0e3997 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -174,7 +174,7 @@ noncomputable def edgeReachability (G : SimpleGraph V) (u v : V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeReachable k u v), k noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := - ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k + ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast From 7015c33aec6ee9a50e8f352536e2a3b0e2dd18d3 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sat, 8 Aug 2026 01:32:22 +0300 Subject: [PATCH 13/63] new theorems and doc strings --- .../Connectivity/EdgeConnectivity.lean | 37 ++++++++++++++++--- 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index c269b9af0e3997..07d998a653614f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -170,26 +170,51 @@ lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u refine (Set.subsingleton_iff_singleton h').mp ?_ exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs) +/-- +The edge reachability number of a graph `G` and two vertices `u`,`v` is the largest `k` for which +`u`,`v` are `k`-edge-reachable +-/ noncomputable def edgeReachability (G : SimpleGraph V) (u v : V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeReachable k u v), k +/-- +The edge connectivity number of a graph `G` is the largest `k` such that `G` is `k`-edge-connected. +-/ noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k -theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by +theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reachable u v) + : 1 ≤ edgeReachability G u v := by + have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h + simp only [ le_iSup_iff , edgeReachability] + intro b h' + specialize h' 1 + grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] + +lemma le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := + le_iSup₂_of_le k h le_rfl + +lemma le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := + le_iSup₂_of_le k h le_rfl + + +theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] +theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] {u v : V} + : G.edgeReachability u v = ⊤ := by + have : u = v := by exact of_decide_eq_true rfl + rw [this] + exact edgeReachability_self + theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm,edgeReachability] -theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := - iSup₂_le ( - fun i hi ↦ - le_iSup₂_of_le i (hi u v) le_rfl - ) +theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := + iSup₂_le fun _ hi ↦ le_edgeReachability (hi u v) /-! From 83f8c364916b3dfc6a08161b1cd77c3941d77fc1 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Fri, 7 Aug 2026 22:33:14 +0000 Subject: [PATCH 14/63] [pre-commit.ci lite] apply automatic fixes --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 07d998a653614f..d068373734fc6b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -213,7 +213,7 @@ theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] {u v : V} theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm,edgeReachability] -theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := +theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ le_edgeReachability (hi u v) From 6d982cd54cce9d91952a4913c505e01cfceadd00 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sat, 8 Aug 2026 01:35:32 +0300 Subject: [PATCH 15/63] ordered --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 07d998a653614f..0cdf936faca5c3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -6,9 +6,9 @@ Authors: Youheng Luo module public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected +public import Mathlib.Data.ENat.Lattice public import Mathlib.Data.Set.Card public import Mathlib.Order.CompletePartialOrder -public import Mathlib.Data.ENat.Lattice /-! # Edge Connectivity @@ -211,12 +211,11 @@ theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] {u v : V} exact edgeReachability_self theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by - simp only [isEdgeReachable_comm,edgeReachability] + simp only [isEdgeReachable_comm, edgeReachability] theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ le_edgeReachability (hi u v) - /-! ### 2-reachability From 02b2272c2d339b31b99422e30a37b51343f8b27e Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sat, 8 Aug 2026 01:37:19 +0300 Subject: [PATCH 16/63] theorems --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 031f82a1f0fcdb..f38dc582b5268b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -191,13 +191,12 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reach specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] -lemma le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := +theorem le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := le_iSup₂_of_le k h le_rfl -lemma le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := +theorem le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := le_iSup₂_of_le k h le_rfl - theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast From d256953ba9602ef6768ed99d89b5c6786952d43f Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sat, 8 Aug 2026 14:37:40 +0300 Subject: [PATCH 17/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f38dc582b5268b..ef8bc930c07897 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -205,9 +205,7 @@ theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] {u v : V} : G.edgeReachability u v = ⊤ := by - have : u = v := by exact of_decide_eq_true rfl - rw [this] - exact edgeReachability_self + simpa [Subsingleton.elim u v] using edgeReachability_self theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm, edgeReachability] From 29f0b1c12767796af1f3afe995b4d71c674e893d Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sun, 9 Aug 2026 02:36:07 +0300 Subject: [PATCH 18/63] le_isup suggestion implemented --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index ef8bc930c07897..cc9c648cd41b34 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -192,10 +192,10 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reach grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] theorem le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := - le_iSup₂_of_le k h le_rfl + le_iSup₂ (α := ℕ∞) k h theorem le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := - le_iSup₂_of_le k h le_rfl + le_iSup₂ (α := ℕ∞) k h theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast From aa329cb4a788d3d2dfd873ac5dbb5b0bb4e20dbc Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 9 Aug 2026 02:37:23 +0300 Subject: [PATCH 19/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index cc9c648cd41b34..e3ecc0e7eb6524 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -203,8 +203,7 @@ theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnect theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] -theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] {u v : V} - : G.edgeReachability u v = ⊤ := by +theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by simpa [Subsingleton.elim u v] using edgeReachability_self theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by From 636c8d0f06194ccd3387cc5695179f9a37edda6d Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 9 Aug 2026 02:37:53 +0300 Subject: [PATCH 20/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index e3ecc0e7eb6524..e99a2602354ce7 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -194,7 +194,7 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reach theorem le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h -theorem le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := +theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := le_iSup₂ (α := ℕ∞) k h theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by From 508b539fc7fcee6349c50a437a3a3b70a83aeb5b Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 9 Aug 2026 02:38:13 +0300 Subject: [PATCH 21/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index e99a2602354ce7..195cea3d062fc3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -191,7 +191,7 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reach specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] -theorem le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := +theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := From 6cdd6552a26b2a48dca396db126049955e44b619 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 9 Aug 2026 02:38:36 +0300 Subject: [PATCH 22/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 195cea3d062fc3..40e4ef765c5265 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -186,7 +186,7 @@ noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reachable u v) : 1 ≤ edgeReachability G u v := by have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h - simp only [ le_iSup_iff , edgeReachability] + simp only [le_iSup_iff, edgeReachability] intro b h' specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] From a6719def1fc87f470acee06af296590bd59b7d9c Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sun, 9 Aug 2026 02:43:45 +0300 Subject: [PATCH 23/63] ne_zero --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index e3ecc0e7eb6524..6009ded1390d7a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -184,7 +184,8 @@ noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reachable u v) - : 1 ≤ edgeReachability G u v := by + : G.edgeReachability u v ≠ 0 := by + rw [Order.one_le_iff_ne_zero.symm] have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h simp only [ le_iSup_iff , edgeReachability] intro b h' From 36fef53ca531cb2a5c9ebcb63d89033182ff3b23 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sun, 9 Aug 2026 13:06:52 +0300 Subject: [PATCH 24/63] fix ci fail --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 6754ea7276f644..e9d043523c8e41 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -192,7 +192,8 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reach specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] -theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := +theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) + : k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := @@ -211,7 +212,7 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u simp only [isEdgeReachable_comm, edgeReachability] theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := - iSup₂_le fun _ hi ↦ le_edgeReachability (hi u v) + iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) /-! ### 2-reachability From 61f75f2653f551b08fa420819cfde182956e259c Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Tue, 11 Aug 2026 01:12:55 +0300 Subject: [PATCH 25/63] 2 more proofs and helper theorem --- .../Connectivity/EdgeConnectivity.lean | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index e9d043523c8e41..f5f4a41e3cd0b5 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -6,6 +6,7 @@ Authors: Youheng Luo module public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected +public import Mathlib.Combinatorics.SimpleGraph.Finite public import Mathlib.Data.ENat.Lattice public import Mathlib.Data.Set.Card public import Mathlib.Order.CompletePartialOrder @@ -214,6 +215,44 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) +theorem notEdgeReachable_degree_plus_one [Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) + : ¬G.IsEdgeReachable (G.degree u + 1) u v := by + intro h + unfold IsEdgeReachable at h + have this2:= @h (G.incidenceSet u) + have : (G.incidenceSet u).encard = G.degree u := by + grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard , Set.coe_ncard_eq_encard] + + rw [this] at this2 + + have := this2 (by simp only [Nat.cast_add, Nat.cast_one] ; exact ENat.natCast_lt_succ ) + rcases this with ⟨p⟩ + cases p with + | nil => + exact huv rfl + | cons h p =>{ + have h' := deleteEdges_adj.mp h + exact h'.2 (by grind [mem_incidenceSet]) + } + +theorem edgeReachability_le_degree_left +[Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) + : G.edgeReachability u v ≤ G.degree u := by + simp only [edgeReachability, iSup_le_iff, Nat.cast_le] + intro i h + have this2 : ¬G.IsEdgeReachable (G.degree u + 1) u v := by + exact notEdgeReachable_degree_plus_one huv + by_contra + simp only [ge_iff_le, not_le] at this + apply this2 + exact IsEdgeReachable.anti this h + +theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] [DecidableEq V] +(huv : u ≠ v) +: G.edgeReachability u v ≤ G.degree v := by + rw [edgeReachability_comm] + exact edgeReachability_le_degree_left (id (Ne.symm huv)) + /-! ### 2-reachability From ddb9601a60c949627b872f831c30c04b49086d0b Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Mon, 10 Aug 2026 22:13:48 +0000 Subject: [PATCH 26/63] [pre-commit.ci lite] apply automatic fixes --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f5f4a41e3cd0b5..1b396b06927c21 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -219,11 +219,11 @@ theorem notEdgeReachable_degree_plus_one [Fintype <| G.neighborSet u] [Decidable : ¬G.IsEdgeReachable (G.degree u + 1) u v := by intro h unfold IsEdgeReachable at h - have this2:= @h (G.incidenceSet u) + have this2:= @h (G.incidenceSet u) have : (G.incidenceSet u).encard = G.degree u := by grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard , Set.coe_ncard_eq_encard] - rw [this] at this2 + rw [this] at this2 have := this2 (by simp only [Nat.cast_add, Nat.cast_one] ; exact ENat.natCast_lt_succ ) rcases this with ⟨p⟩ From 6cc186df116370cd395f29892c1a43df54129350 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Tue, 11 Aug 2026 01:28:25 +0300 Subject: [PATCH 27/63] fix lint style --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 1b396b06927c21..f10c47796d8c26 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -225,7 +225,7 @@ theorem notEdgeReachable_degree_plus_one [Fintype <| G.neighborSet u] [Decidable rw [this] at this2 - have := this2 (by simp only [Nat.cast_add, Nat.cast_one] ; exact ENat.natCast_lt_succ ) + have := this2 (by simp only [Nat.cast_add, Nat.cast_one, ENat.natCast_lt_succ]) rcases this with ⟨p⟩ cases p with | nil => From a3f4d807167c1e3eb18d2d422961d9fbeea7a2a8 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Tue, 11 Aug 2026 01:31:34 +0300 Subject: [PATCH 28/63] fix ci --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f10c47796d8c26..8f61c9716f0689 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -222,9 +222,7 @@ theorem notEdgeReachable_degree_plus_one [Fintype <| G.neighborSet u] [Decidable have this2:= @h (G.incidenceSet u) have : (G.incidenceSet u).encard = G.degree u := by grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard , Set.coe_ncard_eq_encard] - rw [this] at this2 - have := this2 (by simp only [Nat.cast_add, Nat.cast_one, ENat.natCast_lt_succ]) rcases this with ⟨p⟩ cases p with From 35a7e4e25a787a492888e199be2e41fb54466330 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Tue, 11 Aug 2026 23:55:59 +0300 Subject: [PATCH 29/63] suitable name --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 8f61c9716f0689..bec2168588769e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -155,6 +155,7 @@ lemma isEdgeReachable_two : G.IsEdgeReachable 2 u v ↔ ∀ e, (G.deleteEdges {e lemma isEdgeConnected_two : G.IsEdgeConnected 2 ↔ ∀ e, (G.deleteEdges {e}).Preconnected := by simp [isEdgeConnected_add_one] + lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u v) : ∃ w : V, G.Adj u w ∧ G.IsEdgeReachable 2 u w := by obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath @@ -215,7 +216,7 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) -theorem notEdgeReachable_degree_plus_one [Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) +theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by intro h unfold IsEdgeReachable at h @@ -239,7 +240,7 @@ theorem edgeReachability_le_degree_left simp only [edgeReachability, iSup_le_iff, Nat.cast_le] intro i h have this2 : ¬G.IsEdgeReachable (G.degree u + 1) u v := by - exact notEdgeReachable_degree_plus_one huv + exact notEdgeReachable_degree_add_one huv by_contra simp only [ge_iff_le, not_le] at this apply this2 From cf7d0800c04fbffe7e29bf697ed263849b8c33d0 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Wed, 12 Aug 2026 00:02:23 +0300 Subject: [PATCH 30/63] fixing spacing --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index bec2168588769e..d56b2778e5d881 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -216,8 +216,8 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) -theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) - : ¬G.IsEdgeReachable (G.degree u + 1) u v := by +theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableEq V] + (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by intro h unfold IsEdgeReachable at h have this2:= @h (G.incidenceSet u) @@ -234,9 +234,8 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE exact h'.2 (by grind [mem_incidenceSet]) } -theorem edgeReachability_le_degree_left -[Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) - : G.edgeReachability u v ≤ G.degree u := by +theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableEq V] + (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := by simp only [edgeReachability, iSup_le_iff, Nat.cast_le] intro i h have this2 : ¬G.IsEdgeReachable (G.degree u + 1) u v := by @@ -247,8 +246,7 @@ theorem edgeReachability_le_degree_left exact IsEdgeReachable.anti this h theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] [DecidableEq V] -(huv : u ≠ v) -: G.edgeReachability u v ≤ G.degree v := by + (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by rw [edgeReachability_comm] exact edgeReachability_le_degree_left (id (Ne.symm huv)) From 8ac9b7bb03475ca2e91379c5aef3f9e73a702e78 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Tue, 11 Aug 2026 21:03:14 +0000 Subject: [PATCH 31/63] [pre-commit.ci lite] apply automatic fixes --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index d56b2778e5d881..006a560caaa1f0 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -234,7 +234,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE exact h'.2 (by grind [mem_incidenceSet]) } -theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableEq V] +theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := by simp only [edgeReachability, iSup_le_iff, Nat.cast_le] intro i h From d4d2e623666ec65fd98d25b07023787aa4085984 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Wed, 12 Aug 2026 00:12:09 +0300 Subject: [PATCH 32/63] cleaner proof of le_degree_left --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index d56b2778e5d881..80041cec16e5ca 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -234,16 +234,13 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE exact h'.2 (by grind [mem_incidenceSet]) } -theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableEq V] +theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableEq V] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := by simp only [edgeReachability, iSup_le_iff, Nat.cast_le] intro i h - have this2 : ¬G.IsEdgeReachable (G.degree u + 1) u v := by - exact notEdgeReachable_degree_add_one huv - by_contra - simp only [ge_iff_le, not_le] at this - apply this2 - exact IsEdgeReachable.anti this h + by_contra! hcont + apply G.notEdgeReachable_degree_add_one huv + exact IsEdgeReachable.anti hcont h theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] [DecidableEq V] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by From 646a45279c4a78f7f02cc0a38eae1a1d2c023499 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Wed, 12 Aug 2026 15:27:08 +0300 Subject: [PATCH 33/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 80041cec16e5ca..ac0f20ae31c337 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -222,7 +222,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE unfold IsEdgeReachable at h have this2:= @h (G.incidenceSet u) have : (G.incidenceSet u).encard = G.degree u := by - grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard , Set.coe_ncard_eq_encard] + grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard, Set.coe_ncard_eq_encard] rw [this] at this2 have := this2 (by simp only [Nat.cast_add, Nat.cast_one, ENat.natCast_lt_succ]) rcases this with ⟨p⟩ From 1066c78bac1bae346eec1ce85489379a51480df0 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Wed, 12 Aug 2026 15:27:46 +0300 Subject: [PATCH 34/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index ac0f20ae31c337..331613e209a0cc 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -155,7 +155,6 @@ lemma isEdgeReachable_two : G.IsEdgeReachable 2 u v ↔ ∀ e, (G.deleteEdges {e lemma isEdgeConnected_two : G.IsEdgeConnected 2 ↔ ∀ e, (G.deleteEdges {e}).Preconnected := by simp [isEdgeConnected_add_one] - lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u v) : ∃ w : V, G.Adj u w ∧ G.IsEdgeReachable 2 u w := by obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath From a2696f621a2ce0fa626b7afda5ee441d0f286ca9 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Wed, 12 Aug 2026 15:29:56 +0300 Subject: [PATCH 35/63] spacing --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 80041cec16e5ca..78ef0c48e3312a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -185,8 +185,8 @@ The edge connectivity number of a graph `G` is the largest `k` such that `G` is noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k -theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) (h : G.Reachable u v) - : G.edgeReachability u v ≠ 0 := by +theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) + (h : G.Reachable u v) : G.edgeReachability u v ≠ 0 := by rw [Order.one_le_iff_ne_zero.symm] have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h simp only [le_iSup_iff, edgeReachability] From 4ba4c79c953af76ced5829c656ac44c67af85a7c Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Wed, 12 Aug 2026 15:30:30 +0300 Subject: [PATCH 36/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 10e090e1abe79b..4bb706d7ecfb7c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -219,7 +219,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by intro h unfold IsEdgeReachable at h - have this2:= @h (G.incidenceSet u) + have this2 := @h (G.incidenceSet u) have : (G.incidenceSet u).encard = G.degree u := by grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard, Set.coe_ncard_eq_encard] rw [this] at this2 From 375b3cc1e0cf4484ee9670a34ff43018447437ac Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Wed, 12 Aug 2026 15:30:54 +0300 Subject: [PATCH 37/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 4bb706d7ecfb7c..f037fdd6eb494e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -216,7 +216,7 @@ theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReac iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableEq V] - (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by + (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by intro h unfold IsEdgeReachable at h have this2 := @h (G.incidenceSet u) From 52c682f853d16bb64f2307c6b21b397db928a183 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Wed, 12 Aug 2026 15:31:31 +0300 Subject: [PATCH 38/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f037fdd6eb494e..a25dc85a3d863b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -228,7 +228,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE cases p with | nil => exact huv rfl - | cons h p =>{ + | cons h p => { have h' := deleteEdges_adj.mp h exact h'.2 (by grind [mem_incidenceSet]) } From 655b046077348423ff4ddfc22c1e8d8a39b98b1b Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Wed, 12 Aug 2026 15:32:02 +0300 Subject: [PATCH 39/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index a25dc85a3d863b..134a1c43ff3d2d 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -223,8 +223,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE have : (G.incidenceSet u).encard = G.degree u := by grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard, Set.coe_ncard_eq_encard] rw [this] at this2 - have := this2 (by simp only [Nat.cast_add, Nat.cast_one, ENat.natCast_lt_succ]) - rcases this with ⟨p⟩ + have ⟨p⟩ := this2 (by simp only [Nat.cast_add, Nat.cast_one, ENat.natCast_lt_succ]) cases p with | nil => exact huv rfl From d9bbd90eca295b1df5f2855c5e2d372dee54844c Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 13 Aug 2026 18:31:37 +0300 Subject: [PATCH 40/63] finished todo --- .../Connectivity/EdgeConnectivity.lean | 40 ++++++++++++++++--- 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 134a1c43ff3d2d..7beb279674ce3f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -150,11 +150,39 @@ lemma isEdgeReachable_two : G.IsEdgeReachable 2 u v ↔ ∀ e, (G.deleteEdges {e simp [isEdgeReachable_add_one] /-- A graph is 2-edge-connected iff it has no bridge. -/ --- TODO: This should be `G.IsEdgeConnected 2 ↔ ∀ e, ¬G.IsBridge e` after --- https://github.com/leanprover-community/mathlib4/pull/32583 -lemma isEdgeConnected_two : G.IsEdgeConnected 2 ↔ ∀ e, (G.deleteEdges {e}).Preconnected := by +lemma isEdgeConnected_two_iff_Preconnected : + G.IsEdgeConnected 2 ↔ ∀ e, (G.deleteEdges {e}).Preconnected := by simp [isEdgeConnected_add_one] +@[deprecated (since := "2026-08-13")] +alias isEdgeConnected_two := isEdgeConnected_two_iff_Preconnected + +lemma all_notBridge_Preconnected : (∀ e , ¬G.IsBridge e) → G.Preconnected := by + intro h u v + by_contra huv + exact h s(u,v) (IsBridge.of_not_reachable huv) + +/-- A graph is 2-edge-connected iff it has no bridge. -/ +theorem isEdgeConnected_two_iff_notBridge : G.IsEdgeConnected 2 ↔ ∀ e, ¬G.IsBridge e := by + constructor + · intro h + rw [isEdgeConnected_two_iff_Preconnected] at h + intro e + cases e ; expose_names + intro hbridge + exact (isBridge_iff.mp hbridge) (h s(x, y) x y) + · intro h + rw [isEdgeConnected_two_iff_Preconnected] + intro e + cases e ; expose_names + by_cases hV : Nonempty V + · have hG : G.Preconnected := by + exact all_notBridge_Preconnected h + have hG' : G.Connected := G.connected_iff.mpr ⟨hG, hV⟩ + exact (hG'.connected_delete_edge_of_not_isBridge (h (s(x, y)))).preconnected + · intro u v + exact False.elim (hV ⟨u⟩) + lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u v) : ∃ w : V, G.Adj u w ∧ G.IsEdgeReachable 2 u w := by obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath @@ -193,8 +221,8 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] -theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) - : k ≤ G.edgeReachability u v := +theorem IsEdgeReachable.le_edgeReachability + (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := @@ -243,7 +271,7 @@ theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableE theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] [DecidableEq V] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by rw [edgeReachability_comm] - exact edgeReachability_le_degree_left (id (Ne.symm huv)) + exact edgeReachability_le_degree_left huv.symm /-! ### 2-reachability From 7bd77e2aa5688784cf5399ae9949c35f8a192fc5 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Thu, 13 Aug 2026 15:32:44 +0000 Subject: [PATCH 41/63] [pre-commit.ci lite] apply automatic fixes --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 7beb279674ce3f..f69d39ea0da624 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -221,7 +221,7 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] -theorem IsEdgeReachable.le_edgeReachability +theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h From 621ada723d91281d359c7b308221094ec6c2f51b Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 13 Aug 2026 18:41:29 +0300 Subject: [PATCH 42/63] fixed warnings , should pass ci --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 7beb279674ce3f..d63d042db2c48a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -243,8 +243,9 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) -theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableEq V] +theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by + classical intro h unfold IsEdgeReachable at h have this2 := @h (G.incidenceSet u) @@ -260,7 +261,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] [DecidableE exact h'.2 (by grind [mem_incidenceSet]) } -theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableEq V] +theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := by simp only [edgeReachability, iSup_le_iff, Nat.cast_le] intro i h @@ -268,7 +269,7 @@ theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] [DecidableE apply G.notEdgeReachable_degree_add_one huv exact IsEdgeReachable.anti hcont h -theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] [DecidableEq V] +theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by rw [edgeReachability_comm] exact edgeReachability_le_degree_left huv.symm From 40ebccfce357dd46f39c4cd2766d5355f82acbbc Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Thu, 13 Aug 2026 16:08:39 +0000 Subject: [PATCH 43/63] [pre-commit.ci lite] apply automatic fixes --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 3c382baf492878..d6e019fb55e8b6 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -261,7 +261,7 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] exact h'.2 (by grind [mem_incidenceSet]) } -theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] +theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := by simp only [edgeReachability, iSup_le_iff, Nat.cast_le] intro i h From 5d6dc300714f5593c451977f837b7ad458cfb944 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 13 Aug 2026 19:10:08 +0300 Subject: [PATCH 44/63] min imports --- .../Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 3c382baf492878..f39139c3ee2a84 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -6,7 +6,6 @@ Authors: Youheng Luo module public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected -public import Mathlib.Combinatorics.SimpleGraph.Finite public import Mathlib.Data.ENat.Lattice public import Mathlib.Data.Set.Card public import Mathlib.Order.CompletePartialOrder From 2754288a1caae163b17bea4e021b7100ff3b5479 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 13 Aug 2026 19:19:05 +0300 Subject: [PATCH 45/63] space before semicolon --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f39139c3ee2a84..e6cad704135eb3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -167,13 +167,13 @@ theorem isEdgeConnected_two_iff_notBridge : G.IsEdgeConnected 2 ↔ ∀ e, ¬G.I · intro h rw [isEdgeConnected_two_iff_Preconnected] at h intro e - cases e ; expose_names + cases e; expose_names intro hbridge exact (isBridge_iff.mp hbridge) (h s(x, y) x y) · intro h rw [isEdgeConnected_two_iff_Preconnected] intro e - cases e ; expose_names + cases e; expose_names by_cases hV : Nonempty V · have hG : G.Preconnected := by exact all_notBridge_Preconnected h From a0561a4fa56dd4b7bf29a655ad2eca00b58d11f3 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Thu, 13 Aug 2026 19:45:55 +0300 Subject: [PATCH 46/63] start ci From 3b6fd35982d459e6a60f088fef2314acee5df23f Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sat, 15 Aug 2026 14:41:19 +0300 Subject: [PATCH 47/63] edgeconnectivity_le_mindegree --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index e2d54fde66b272..c73acb885679c5 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -273,6 +273,15 @@ theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] rw [edgeReachability_comm] exact edgeReachability_le_degree_left huv.symm +theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] + [DecidableRel G.Adj] : G.edgeConnectivity ≤ G.minDegree := by + apply iSup₂_le + intro i h + simp only [Nat.cast_le] + apply le_minDegree_of_forall_le_degree + intro v + apply IsEdgeConnected.le_degree h + /-! ### 2-reachability From 9dd49c0e10d603a29c5eb4659e6d014c7f33758a Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 16 Aug 2026 21:06:23 +0300 Subject: [PATCH 48/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index c73acb885679c5..ec471ea58b7d55 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -156,7 +156,7 @@ lemma isEdgeConnected_two_iff_Preconnected : @[deprecated (since := "2026-08-13")] alias isEdgeConnected_two := isEdgeConnected_two_iff_Preconnected -lemma all_notBridge_Preconnected : (∀ e , ¬G.IsBridge e) → G.Preconnected := by +lemma all_notBridge_Preconnected : (∀ e, ¬G.IsBridge e) → G.Preconnected := by intro h u v by_contra huv exact h s(u,v) (IsBridge.of_not_reachable huv) From af7a0acc88fcd1372c630da45973a1815f464e04 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 16 Aug 2026 21:20:13 +0300 Subject: [PATCH 49/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index ec471ea58b7d55..21b19f8e75fc6e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -261,12 +261,8 @@ theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] } theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] - (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := by - simp only [edgeReachability, iSup_le_iff, Nat.cast_le] - intro i h - by_contra! hcont - apply G.notEdgeReachable_degree_add_one huv - exact IsEdgeReachable.anti hcont h + (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := + iSup₂_le fun _ hk ↦ mod_cast hk.le_degree huv theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by From 62e56ff43e4fbbf38cd9ccc242f4fdc928609e09 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sun, 16 Aug 2026 21:21:34 +0300 Subject: [PATCH 50/63] remove notedgereachable --- .../Connectivity/EdgeConnectivity.lean | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 21b19f8e75fc6e..8663efbe0fe288 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -242,24 +242,6 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) -theorem notEdgeReachable_degree_add_one [Fintype <| G.neighborSet u] - (huv : u ≠ v) : ¬G.IsEdgeReachable (G.degree u + 1) u v := by - classical - intro h - unfold IsEdgeReachable at h - have this2 := @h (G.incidenceSet u) - have : (G.incidenceSet u).encard = G.degree u := by - grind [card_incidenceSet_eq_degree, Set.coe_fintypeCard, Set.coe_ncard_eq_encard] - rw [this] at this2 - have ⟨p⟩ := this2 (by simp only [Nat.cast_add, Nat.cast_one, ENat.natCast_lt_succ]) - cases p with - | nil => - exact huv rfl - | cons h p => { - have h' := deleteEdges_adj.mp h - exact h'.2 (by grind [mem_incidenceSet]) - } - theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := iSup₂_le fun _ hk ↦ mod_cast hk.le_degree huv From 18019379d9dcc4168e9bbad20f1e45da5d5b5bfd Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 16 Aug 2026 21:22:18 +0300 Subject: [PATCH 51/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 8663efbe0fe288..c410fabac2b10c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -251,8 +251,8 @@ theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] rw [edgeReachability_comm] exact edgeReachability_le_degree_left huv.symm -theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] - [DecidableRel G.Adj] : G.edgeConnectivity ≤ G.minDegree := by +theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] [DecidableRel G.Adj] : + G.edgeConnectivity ≤ G.minDegree := by apply iSup₂_le intro i h simp only [Nat.cast_le] From cb2499b790bac0f748170dd30fa8b97ea2e425cb Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 16 Aug 2026 21:22:59 +0300 Subject: [PATCH 52/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index c410fabac2b10c..80a0480c07c229 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -220,8 +220,8 @@ theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) specialize h' 1 grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] -theorem IsEdgeReachable.le_edgeReachability - (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := +theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) : + k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := From 07809f59ba0f1079f50b0f884095f159f68f036f Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sun, 16 Aug 2026 21:23:35 +0300 Subject: [PATCH 53/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 80a0480c07c229..ce0a3b97aeaed0 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -211,8 +211,7 @@ The edge connectivity number of a graph `G` is the largest `k` such that `G` is noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k -theorem edgeReachability_of_Reachable (G : SimpleGraph V) (u v : V) - (h : G.Reachable u v) : G.edgeReachability u v ≠ 0 := by +theorem Reachable.edgeReachability_ne_zero (h : G.Reachable u v) : G.edgeReachability u v ≠ 0 := by rw [Order.one_le_iff_ne_zero.symm] have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h simp only [le_iSup_iff, edgeReachability] From 04a117211c44416871592171e54e3679ff92d81d Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sun, 16 Aug 2026 21:39:23 +0300 Subject: [PATCH 54/63] extracting lemma --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 8663efbe0fe288..d9612216a8aad8 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -107,6 +107,10 @@ lemma IsEdgeConnected.le_degree [Fintype (G.neighborSet u)] [Nontrivial V] obtain ⟨v, hv⟩ := exists_ne u exact (h u v).le_degree hv.symm +theorem IsEdgeConnected.le_minDegree [Fintype V] [Nontrivial V] + [DecidableRel G.Adj] (h : G.IsEdgeConnected k) : + k ≤ G.minDegree := le_minDegree_of_forall_le_degree G k fun _ ↦ le_degree h + lemma isEdgeReachable_add_one (hk : k ≠ 0) : G.IsEdgeReachable (k + 1) u v ↔ ∀ e, (G.deleteEdges {e}).IsEdgeReachable k u v := by refine ⟨fun h e s hk ↦ ?_, fun h s hs ↦ ?_⟩ @@ -251,14 +255,8 @@ theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] rw [edgeReachability_comm] exact edgeReachability_le_degree_left huv.symm -theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] - [DecidableRel G.Adj] : G.edgeConnectivity ≤ G.minDegree := by - apply iSup₂_le - intro i h - simp only [Nat.cast_le] - apply le_minDegree_of_forall_le_degree - intro v - apply IsEdgeConnected.le_degree h +theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] [DecidableRel G.Adj] : + G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast (IsEdgeConnected.le_minDegree h) /-! ### 2-reachability From 9eb8d6256ebccf6d0b7a1bd0c6f2f9c92f573e66 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Sun, 16 Aug 2026 21:49:32 +0300 Subject: [PATCH 55/63] todo solution moved to another PR --- .../Connectivity/EdgeConnectivity.lean | 34 ++----------------- 1 file changed, 3 insertions(+), 31 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index e1a863ac41080b..dc691cafd08612 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -153,39 +153,11 @@ lemma isEdgeReachable_two : G.IsEdgeReachable 2 u v ↔ ∀ e, (G.deleteEdges {e simp [isEdgeReachable_add_one] /-- A graph is 2-edge-connected iff it has no bridge. -/ -lemma isEdgeConnected_two_iff_Preconnected : - G.IsEdgeConnected 2 ↔ ∀ e, (G.deleteEdges {e}).Preconnected := by +-- TODO: This should be `G.IsEdgeConnected 2 ↔ ∀ e, ¬G.IsBridge e` after +-- https://github.com/leanprover-community/mathlib4/pull/32583 +lemma isEdgeConnected_two : G.IsEdgeConnected 2 ↔ ∀ e, (G.deleteEdges {e}).Preconnected := by simp [isEdgeConnected_add_one] -@[deprecated (since := "2026-08-13")] -alias isEdgeConnected_two := isEdgeConnected_two_iff_Preconnected - -lemma all_notBridge_Preconnected : (∀ e, ¬G.IsBridge e) → G.Preconnected := by - intro h u v - by_contra huv - exact h s(u,v) (IsBridge.of_not_reachable huv) - -/-- A graph is 2-edge-connected iff it has no bridge. -/ -theorem isEdgeConnected_two_iff_notBridge : G.IsEdgeConnected 2 ↔ ∀ e, ¬G.IsBridge e := by - constructor - · intro h - rw [isEdgeConnected_two_iff_Preconnected] at h - intro e - cases e; expose_names - intro hbridge - exact (isBridge_iff.mp hbridge) (h s(x, y) x y) - · intro h - rw [isEdgeConnected_two_iff_Preconnected] - intro e - cases e; expose_names - by_cases hV : Nonempty V - · have hG : G.Preconnected := by - exact all_notBridge_Preconnected h - have hG' : G.Connected := G.connected_iff.mpr ⟨hG, hV⟩ - exact (hG'.connected_delete_edge_of_not_isBridge (h (s(x, y)))).preconnected - · intro u v - exact False.elim (hV ⟨u⟩) - lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u v) : ∃ w : V, G.Adj u w ∧ G.IsEdgeReachable 2 u w := by obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath From ee19d104bb34ce02e418710f98142beff2752875 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Tue, 18 Aug 2026 18:56:57 +0300 Subject: [PATCH 56/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index dc691cafd08612..daa7cb4ea0ff22 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -107,9 +107,9 @@ lemma IsEdgeConnected.le_degree [Fintype (G.neighborSet u)] [Nontrivial V] obtain ⟨v, hv⟩ := exists_ne u exact (h u v).le_degree hv.symm -theorem IsEdgeConnected.le_minDegree [Fintype V] [Nontrivial V] - [DecidableRel G.Adj] (h : G.IsEdgeConnected k) : - k ≤ G.minDegree := le_minDegree_of_forall_le_degree G k fun _ ↦ le_degree h +theorem IsEdgeConnected.le_minDegree [Fintype V] [Nontrivial V] [DecidableRel G.Adj] + (h : G.IsEdgeConnected k) : k ≤ G.minDegree := + le_minDegree_of_forall_le_degree G k fun _ ↦ le_degree h lemma isEdgeReachable_add_one (hk : k ≠ 0) : G.IsEdgeReachable (k + 1) u v ↔ ∀ e, (G.deleteEdges {e}).IsEdgeReachable k u v := by From 9be639bf2d5228a047ee904c7abcf5123cbdd5f0 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Tue, 18 Aug 2026 18:57:29 +0300 Subject: [PATCH 57/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index daa7cb4ea0ff22..c00e641c9bac94 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -217,8 +217,8 @@ theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u theorem edgeConnectivity_le_edgeReachability : G.edgeConnectivity ≤ G.edgeReachability u v := iSup₂_le fun _ hi ↦ IsEdgeReachable.le_edgeReachability (hi u v) -theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] - (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u := +theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] (huv : u ≠ v) : + G.edgeReachability u v ≤ G.degree u := iSup₂_le fun _ hk ↦ mod_cast hk.le_degree huv theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] From 0bb5b1f1593b013ab60f4033bbcb0c20e77f7286 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Tue, 18 Aug 2026 18:58:01 +0300 Subject: [PATCH 58/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index c00e641c9bac94..f1f205d601d636 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -221,8 +221,8 @@ theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] (huv : u G.edgeReachability u v ≤ G.degree u := iSup₂_le fun _ hk ↦ mod_cast hk.le_degree huv -theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] - (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by +theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] (huv : u ≠ v) : + G.edgeReachability u v ≤ G.degree v := by rw [edgeReachability_comm] exact edgeReachability_le_degree_left huv.symm From 147abd2d2c8b779f98304dffb2186feaf64381c8 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Tue, 18 Aug 2026 18:58:25 +0300 Subject: [PATCH 59/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index f1f205d601d636..a552981da1b377 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -227,7 +227,7 @@ theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] (huv : u exact edgeReachability_le_degree_left huv.symm theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] [DecidableRel G.Adj] : - G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast (IsEdgeConnected.le_minDegree h) + G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast h.le_minDegree /-! ### 2-reachability From 41578bc7d9ea12ebf4114c4e1cccbe238e7ef7d3 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Tue, 18 Aug 2026 19:42:36 +0300 Subject: [PATCH 60/63] simp lemma --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index dc691cafd08612..da625dd28b4b34 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -205,11 +205,12 @@ theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G. theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast +@[simp] theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by - simpa [Subsingleton.elim u v] using edgeReachability_self + simp [Subsingleton.elim u v] theorem edgeReachability_comm : G.edgeReachability u v = G.edgeReachability v u := by simp only [isEdgeReachable_comm, edgeReachability] From 7335512288d43351982532e3bdcdf0f1eec0e601 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Tue, 18 Aug 2026 19:43:00 +0300 Subject: [PATCH 61/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index a552981da1b377..a88a3a78f278f8 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -202,6 +202,7 @@ theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) : theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := le_iSup₂ (α := ℕ∞) k h +@[simp] theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast From b66439d65ecc873c0192cfab999af2149586718f Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Tue, 18 Aug 2026 19:45:20 +0300 Subject: [PATCH 62/63] Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- .../Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 9780590326dc4a..0da31883567e39 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -210,6 +210,7 @@ theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnect theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast] +@[simp] theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by simp [Subsingleton.elim u v] From aa9e05e6db4d0a531cb975e523df20ffc3049ca6 Mon Sep 17 00:00:00 2001 From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com> Date: Tue, 18 Aug 2026 19:49:58 +0300 Subject: [PATCH 63/63] simpler proof --- .../SimpleGraph/Connectivity/EdgeConnectivity.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index 0da31883567e39..02f9e238a6ed9b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -187,18 +187,13 @@ The edge connectivity number of a graph `G` is the largest `k` such that `G` is noncomputable def edgeConnectivity (G : SimpleGraph V) : ℕ∞ := ⨆ (k : ℕ) (_ : G.IsEdgeConnected k), k -theorem Reachable.edgeReachability_ne_zero (h : G.Reachable u v) : G.edgeReachability u v ≠ 0 := by - rw [Order.one_le_iff_ne_zero.symm] - have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h - simp only [le_iSup_iff, edgeReachability] - intro b h' - specialize h' 1 - grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff] - theorem IsEdgeReachable.le_edgeReachability (h : G.IsEdgeReachable k u v) : k ≤ G.edgeReachability u v := le_iSup₂ (α := ℕ∞) k h +theorem Reachable.edgeReachability_ne_zero (h : G.Reachable u v) : G.edgeReachability u v ≠ 0 := by + simpa [← Order.one_le_iff_ne_zero] using isEdgeReachable_one.mpr h |>.le_edgeReachability + theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity := le_iSup₂ (α := ℕ∞) k h