From 04cea0add8c2df47a6fbdbac9e1f04771d68c0e8 Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Fri, 22 May 2026 11:50:18 +0200 Subject: [PATCH 1/4] Add in lemma --- Mathlib/Topology/Connected/Basic.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index ac1c869416295e..041044fae85d61 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -200,6 +200,26 @@ theorem IsConnected.iUnion_of_reflTransGen {ι : Type*} [Nonempty ι] {s : ι ⟨nonempty_iUnion.2 <| Nonempty.elim ‹_› fun i : ι => ⟨i, (H _).nonempty⟩, IsPreconnected.iUnion_of_reflTransGen (fun i => (H i).isPreconnected) K⟩ +lemma IsPreconnected.transGen_of_iUnion {ι : Type*} {s : ι → Set α} + (hs : IsPreconnected (⋃ n, s n)) (hs' : ∀ i, IsOpen (s i)) (i j : ι) (hi : (s i).Nonempty) + (hj : (s j).Nonempty) : TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j := by + by_contra hij + let S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k} + let U : Set α := ⋃ k ∈ S, s k + let V : Set α := ⋃ k ∈ Sᶜ, s k + have hsplit : iUnion s = U ∪ V := iSup_split s (· ∈ S) + obtain ⟨a, ha⟩ := hi + obtain ⟨b, hb⟩ := hj + let hi_S : i ∈ S := Relation.TransGen.single ⟨a, ha, ha⟩ + have hUne : ((iUnion s) ∩ U).Nonempty := ⟨a, mem_iUnion_of_mem i ha, mem_iUnion₂_of_mem hi_S ha⟩ + have hVne : ((iUnion s) ∩ V).Nonempty := ⟨b, mem_iUnion_of_mem j hb, mem_iUnion₂_of_mem hij hb⟩ + obtain ⟨x, -, hxU, hxV⟩ := hs U V (isOpen_biUnion fun i a ↦ hs' i) + (isOpen_biUnion fun i a ↦ hs' i) hsplit.le hUne hVne + simp only [mem_iUnion, exists_prop, mem_compl_iff, U, V] at hxU hxV + obtain ⟨k, hk, hxk⟩ := hxU + obtain ⟨l, hl, hxl⟩ := hxV + exact hl (hk.tail ⟨x, hxk, hxl⟩) + section SuccOrder open Order From fa49e11d47c20f5bd9bdfdc76f12c1a48eba7fa0 Mon Sep 17 00:00:00 2001 From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com> Date: Sat, 23 May 2026 13:45:23 +0200 Subject: [PATCH 2/4] Update Mathlib/Topology/Connected/Basic.lean Co-authored-by: Aaron Liu --- Mathlib/Topology/Connected/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 041044fae85d61..eeb4e649071bef 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -200,7 +200,7 @@ theorem IsConnected.iUnion_of_reflTransGen {ι : Type*} [Nonempty ι] {s : ι ⟨nonempty_iUnion.2 <| Nonempty.elim ‹_› fun i : ι => ⟨i, (H _).nonempty⟩, IsPreconnected.iUnion_of_reflTransGen (fun i => (H i).isPreconnected) K⟩ -lemma IsPreconnected.transGen_of_iUnion {ι : Type*} {s : ι → Set α} +lemma IsPreconnected.transGen_of_iUnion {ι : Sort*} {s : ι → Set α} (hs : IsPreconnected (⋃ n, s n)) (hs' : ∀ i, IsOpen (s i)) (i j : ι) (hi : (s i).Nonempty) (hj : (s j).Nonempty) : TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j := by by_contra hij From 044384de17b16f020ce9bed997c1134f1935bb75 Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Sat, 23 May 2026 13:51:33 +0200 Subject: [PATCH 3/4] Revert change which caused some issues --- Mathlib/Topology/Connected/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index eeb4e649071bef..041044fae85d61 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -200,7 +200,7 @@ theorem IsConnected.iUnion_of_reflTransGen {ι : Type*} [Nonempty ι] {s : ι ⟨nonempty_iUnion.2 <| Nonempty.elim ‹_› fun i : ι => ⟨i, (H _).nonempty⟩, IsPreconnected.iUnion_of_reflTransGen (fun i => (H i).isPreconnected) K⟩ -lemma IsPreconnected.transGen_of_iUnion {ι : Sort*} {s : ι → Set α} +lemma IsPreconnected.transGen_of_iUnion {ι : Type*} {s : ι → Set α} (hs : IsPreconnected (⋃ n, s n)) (hs' : ∀ i, IsOpen (s i)) (i j : ι) (hi : (s i).Nonempty) (hj : (s j).Nonempty) : TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j := by by_contra hij From 0ec643349a1a1447e79d2b3e7607b0555c31a285 Mon Sep 17 00:00:00 2001 From: Raph-DG Date: Sun, 24 May 2026 20:02:41 +0200 Subject: [PATCH 4/4] Made iUnion notation consistent --- Mathlib/Topology/Connected/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 041044fae85d61..b428bfcdbbf6c2 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -207,12 +207,12 @@ lemma IsPreconnected.transGen_of_iUnion {ι : Type*} {s : ι → Set α} let S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k} let U : Set α := ⋃ k ∈ S, s k let V : Set α := ⋃ k ∈ Sᶜ, s k - have hsplit : iUnion s = U ∪ V := iSup_split s (· ∈ S) + have hsplit : (⋃ n, s n) = U ∪ V := iSup_split s (· ∈ S) obtain ⟨a, ha⟩ := hi obtain ⟨b, hb⟩ := hj let hi_S : i ∈ S := Relation.TransGen.single ⟨a, ha, ha⟩ - have hUne : ((iUnion s) ∩ U).Nonempty := ⟨a, mem_iUnion_of_mem i ha, mem_iUnion₂_of_mem hi_S ha⟩ - have hVne : ((iUnion s) ∩ V).Nonempty := ⟨b, mem_iUnion_of_mem j hb, mem_iUnion₂_of_mem hij hb⟩ + have hUne : ((⋃ n, s n) ∩ U).Nonempty := ⟨a, mem_iUnion_of_mem i ha, mem_iUnion₂_of_mem hi_S ha⟩ + have hVne : ((⋃ n, s n) ∩ V).Nonempty := ⟨b, mem_iUnion_of_mem j hb, mem_iUnion₂_of_mem hij hb⟩ obtain ⟨x, -, hxU, hxV⟩ := hs U V (isOpen_biUnion fun i a ↦ hs' i) (isOpen_biUnion fun i a ↦ hs' i) hsplit.le hUne hVne simp only [mem_iUnion, exists_prop, mem_compl_iff, U, V] at hxU hxV