From c970ea7008551860ab7b33dc9bfb689f3a5145a8 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 23 Jan 2024 15:18:52 -0800 Subject: [PATCH 1/3] refactor(Topology/Clopen): order of open and closed --- Mathlib/FieldTheory/KrullTopology.lean | 2 +- Mathlib/Topology/AlexandrovDiscrete.lean | 8 +-- Mathlib/Topology/Algebra/OpenSubgroup.lean | 2 +- Mathlib/Topology/Clopen.lean | 53 +++++++++---------- Mathlib/Topology/ClopenBox.lean | 4 +- Mathlib/Topology/CompactOpen.lean | 2 +- Mathlib/Topology/Connected/Basic.lean | 18 +++---- .../Topology/Connected/LocallyConnected.lean | 2 +- Mathlib/Topology/Connected/PathConnected.lean | 10 ++-- .../Connected/TotallyDisconnected.lean | 2 +- Mathlib/Topology/DiscreteQuotient.lean | 4 +- Mathlib/Topology/LocallyConstant/Basic.lean | 6 +-- Mathlib/Topology/SeparatedMap.lean | 2 +- Mathlib/Topology/Separation.lean | 20 +++---- Mathlib/Topology/Sets/Compacts.lean | 2 +- Mathlib/Topology/StoneCech.lean | 2 +- 16 files changed, 69 insertions(+), 70 deletions(-) diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean index ebca4adc56ca2..91c71463548f3 100644 --- a/Mathlib/FieldTheory/KrullTopology.lean +++ b/Mathlib/FieldTheory/KrullTopology.lean @@ -267,7 +267,7 @@ theorem krullTopology_totallyDisconnected {K L : Type*} [Field K] [Field L] [Alg let E := IntermediateField.adjoin K ({x} : Set L) haveI := IntermediateField.adjoin.finiteDimensional (h_int x) refine' ⟨σ • E.fixingSubgroup, - ⟨E.fixingSubgroup_isOpen.leftCoset σ, E.fixingSubgroup_isClosed.leftCoset σ⟩, + ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩, ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, _⟩ simp only [mem_leftCoset_iff, SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff, not_forall] diff --git a/Mathlib/Topology/AlexandrovDiscrete.lean b/Mathlib/Topology/AlexandrovDiscrete.lean index e4dc0a9f35bf7..0349d90368a04 100644 --- a/Mathlib/Topology/AlexandrovDiscrete.lean +++ b/Mathlib/Topology/AlexandrovDiscrete.lean @@ -80,20 +80,20 @@ lemma isClosed_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClosed (f isClosed_iUnion fun _ ↦ isClosed_iUnion <| hf _ lemma isClopen_sInter (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋂₀ S) := - ⟨isOpen_sInter fun s hs ↦ (hS s hs).1, isClosed_sInter fun s hs ↦ (hS s hs).2⟩ + ⟨isClosed_sInter fun s hs ↦ (hS s hs).1, isOpen_sInter fun s hs ↦ (hS s hs).2⟩ lemma isClopen_iInter (hf : ∀ i, IsClopen (f i)) : IsClopen (⋂ i, f i) := - ⟨isOpen_iInter fun i ↦ (hf i).1, isClosed_iInter fun i ↦ (hf i).2⟩ + ⟨isClosed_iInter fun i ↦ (hf i).1, isOpen_iInter fun i ↦ (hf i).2⟩ lemma isClopen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) : IsClopen (⋂ i, ⋂ j, f i j) := isClopen_iInter fun _ ↦ isClopen_iInter <| hf _ lemma isClopen_sUnion (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋃₀ S) := - ⟨isOpen_sUnion fun s hs ↦ (hS s hs).1, isClosed_sUnion fun s hs ↦ (hS s hs).2⟩ + ⟨isClosed_sUnion fun s hs ↦ (hS s hs).1, isOpen_sUnion fun s hs ↦ (hS s hs).2⟩ lemma isClopen_iUnion (hf : ∀ i, IsClopen (f i)) : IsClopen (⋃ i, f i) := - ⟨isOpen_iUnion fun i ↦ (hf i).1, isClosed_iUnion fun i ↦ (hf i).2⟩ + ⟨isClosed_iUnion fun i ↦ (hf i).1, isOpen_iUnion fun i ↦ (hf i).2⟩ lemma isClopen_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) : IsClopen (⋃ i, ⋃ j, f i j) := diff --git a/Mathlib/Topology/Algebra/OpenSubgroup.lean b/Mathlib/Topology/Algebra/OpenSubgroup.lean index 208e0e1b86ca8..dc9e0082c546c 100644 --- a/Mathlib/Topology/Algebra/OpenSubgroup.lean +++ b/Mathlib/Topology/Algebra/OpenSubgroup.lean @@ -179,7 +179,7 @@ theorem isClosed [ContinuousMul G] (U : OpenSubgroup G) : IsClosed (U : Set G) : @[to_additive] theorem isClopen [ContinuousMul G] (U : OpenSubgroup G) : IsClopen (U : Set G) := - ⟨U.isOpen, U.isClosed⟩ + ⟨U.isClosed, U.isOpen⟩ #align open_subgroup.is_clopen OpenSubgroup.isClopen #align open_add_subgroup.is_clopen OpenAddSubgroup.isClopen diff --git a/Mathlib/Topology/Clopen.lean b/Mathlib/Topology/Clopen.lean index 4dd807e3000d5..ae126904aa985 100644 --- a/Mathlib/Topology/Clopen.lean +++ b/Mathlib/Topology/Clopen.lean @@ -9,7 +9,7 @@ import Mathlib.Data.Set.BoolIndicator /-! # Clopen sets -A clopen set is a set that is both open and closed. +A clopen set is a set that is both closed and open. -/ open Set Filter Topology TopologicalSpace Classical @@ -22,23 +22,22 @@ variable [TopologicalSpace X] [TopologicalSpace Y] {s t : Set X} section Clopen --- porting note: todo: redefine as `IsClosed s ∧ IsOpen s` -/-- A set is clopen if it is both open and closed. -/ +/-- A set is clopen if it is both closed and open. -/ def IsClopen (s : Set X) : Prop := - IsOpen s ∧ IsClosed s + IsClosed s ∧ IsOpen s #align is_clopen IsClopen -protected theorem IsClopen.isOpen (hs : IsClopen s) : IsOpen s := hs.1 +protected theorem IsClopen.isOpen (hs : IsClopen s) : IsOpen s := hs.2 #align is_clopen.is_open IsClopen.isOpen -protected theorem IsClopen.isClosed (hs : IsClopen s) : IsClosed s := hs.2 +protected theorem IsClopen.isClosed (hs : IsClopen s) : IsClosed s := hs.1 #align is_clopen.is_closed IsClopen.isClosed theorem isClopen_iff_frontier_eq_empty : IsClopen s ↔ frontier s = ∅ := by rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty] - refine' ⟨fun h => (h.2.trans h.1.symm).subset, fun h => _⟩ - exact ⟨interior_subset.antisymm (subset_closure.trans h), - (h.trans interior_subset).antisymm subset_closure⟩ + refine' ⟨fun h => (h.1.trans h.2.symm).subset, fun h => _⟩ + exact ⟨(h.trans interior_subset).antisymm subset_closure, + interior_subset.antisymm (subset_closure.trans h)⟩ #align is_clopen_iff_frontier_eq_empty isClopen_iff_frontier_eq_empty @[simp] alias ⟨IsClopen.frontier_eq, _⟩ := isClopen_iff_frontier_eq_empty @@ -52,14 +51,14 @@ theorem IsClopen.inter (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ t) ⟨hs.1.inter ht.1, hs.2.inter ht.2⟩ #align is_clopen.inter IsClopen.inter -theorem isClopen_empty : IsClopen (∅ : Set X) := ⟨isOpen_empty, isClosed_empty⟩ +theorem isClopen_empty : IsClopen (∅ : Set X) := ⟨isClosed_empty, isOpen_empty⟩ #align is_clopen_empty isClopen_empty -theorem isClopen_univ : IsClopen (univ : Set X) := ⟨isOpen_univ, isClosed_univ⟩ +theorem isClopen_univ : IsClopen (univ : Set X) := ⟨isClosed_univ, isOpen_univ⟩ #align is_clopen_univ isClopen_univ theorem IsClopen.compl (hs : IsClopen s) : IsClopen sᶜ := - ⟨hs.2.isOpen_compl, hs.1.isClosed_compl⟩ + ⟨hs.2.isClosed_compl, hs.1.isOpen_compl⟩ #align is_clopen.compl IsClopen.compl @[simp] @@ -77,12 +76,12 @@ theorem IsClopen.prod {t : Set Y} (hs : IsClopen s) (ht : IsClopen t) : IsClopen theorem isClopen_iUnion_of_finite [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋃ i, s i) := - ⟨isOpen_iUnion (forall_and.1 h).1, isClosed_iUnion_of_finite (forall_and.1 h).2⟩ + ⟨isClosed_iUnion_of_finite (forall_and.1 h).1, isOpen_iUnion (forall_and.1 h).2⟩ #align is_clopen_Union isClopen_iUnion_of_finite theorem Set.Finite.isClopen_biUnion {s : Set Y} {f : Y → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i) := - ⟨isOpen_biUnion fun i hi => (h i hi).1, hs.isClosed_biUnion fun i hi => (h i hi).2⟩ + ⟨hs.isClosed_biUnion fun i hi => (h i hi).1, isOpen_biUnion fun i hi => (h i hi).2⟩ #align is_clopen_bUnion Set.Finite.isClopen_biUnion theorem isClopen_biUnion_finset {s : Finset Y} {f : Y → Set X} @@ -92,12 +91,12 @@ theorem isClopen_biUnion_finset {s : Finset Y} {f : Y → Set X} theorem isClopen_iInter_of_finite [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋂ i, s i) := - ⟨isOpen_iInter_of_finite (forall_and.1 h).1, isClosed_iInter (forall_and.1 h).2⟩ + ⟨isClosed_iInter (forall_and.1 h).1, isOpen_iInter_of_finite (forall_and.1 h).2⟩ #align is_clopen_Inter isClopen_iInter_of_finite theorem Set.Finite.isClopen_biInter {s : Set Y} (hs : s.Finite) {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i) := - ⟨hs.isOpen_biInter fun i hi => (h i hi).1, isClosed_biInter fun i hi => (h i hi).2⟩ + ⟨isClosed_biInter fun i hi => (h i hi).1, hs.isOpen_biInter fun i hi => (h i hi).2⟩ #align is_clopen_bInter Set.Finite.isClopen_biInter theorem isClopen_biInter_finset {s : Finset Y} {f : Y → Set X} @@ -112,15 +111,15 @@ theorem IsClopen.preimage {s : Set Y} (h : IsClopen s) {f : X → Y} (hf : Conti theorem ContinuousOn.preimage_isClopen_of_isClopen {f : X → Y} {s : Set X} {t : Set Y} (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t) := - ⟨ContinuousOn.isOpen_inter_preimage hf hs.1 ht.1, - ContinuousOn.preimage_isClosed_of_isClosed hf hs.2 ht.2⟩ + ⟨ContinuousOn.preimage_isClosed_of_isClosed hf hs.1 ht.1, + ContinuousOn.isOpen_inter_preimage hf hs.2 ht.2⟩ #align continuous_on.preimage_clopen_of_clopen ContinuousOn.preimage_isClopen_of_isClopen /-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen. -/ theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen (s ∩ a) := by - refine' ⟨IsOpen.inter h.1 ha, _⟩ - have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.2 (isClosed_compl_iff.2 hb) + refine' ⟨_, IsOpen.inter h.2 ha⟩ + have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb) convert this using 1 refine' (inter_subset_inter_right s hab.subset_compl_right).antisymm _ rintro x ⟨hx₁, hx₂⟩ @@ -129,25 +128,25 @@ theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) @[simp] theorem isClopen_discrete [DiscreteTopology X] (s : Set X) : IsClopen s := - ⟨isOpen_discrete _, isClosed_discrete _⟩ + ⟨isClosed_discrete _, isOpen_discrete _⟩ #align is_clopen_discrete isClopen_discrete -- porting note: new lemma theorem isClopen_range_inl : IsClopen (range (Sum.inl : X → X ⊕ Y)) := - ⟨isOpen_range_inl, isClosed_range_inl⟩ + ⟨isClosed_range_inl, isOpen_range_inl⟩ -- porting note: new lemma theorem isClopen_range_inr : IsClopen (range (Sum.inr : Y → X ⊕ Y)) := - ⟨isOpen_range_inr, isClosed_range_inr⟩ + ⟨isClosed_range_inr, isOpen_range_inr⟩ theorem isClopen_range_sigmaMk {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {i : ι} : IsClopen (Set.range (@Sigma.mk ι X i)) := - ⟨openEmbedding_sigmaMk.open_range, closedEmbedding_sigmaMk.closed_range⟩ + ⟨closedEmbedding_sigmaMk.closed_range, openEmbedding_sigmaMk.open_range⟩ #align clopen_range_sigma_mk isClopen_range_sigmaMk protected theorem QuotientMap.isClopen_preimage {f : X → Y} (hf : QuotientMap f) {s : Set Y} : IsClopen (f ⁻¹' s) ↔ IsClopen s := - and_congr hf.isOpen_preimage hf.isClosed_preimage + and_congr hf.isClosed_preimage hf.isOpen_preimage #align quotient_map.is_clopen_preimage QuotientMap.isClopen_preimage theorem continuous_boolIndicator_iff_isClopen (U : Set X) : @@ -155,10 +154,10 @@ theorem continuous_boolIndicator_iff_isClopen (U : Set X) : constructor · intro hc rw [← U.preimage_boolIndicator_true] - exact ⟨(isOpen_discrete _).preimage hc, (isClosed_discrete _).preimage hc⟩ + exact ⟨(isClosed_discrete _).preimage hc, (isOpen_discrete _).preimage hc, ⟩ · refine' fun hU => ⟨fun s _ => _⟩ rcases U.preimage_boolIndicator s with (h | h | h | h) <;> rw [h] - exacts [isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty] + exacts [isOpen_univ, hU.2, hU.1.isOpen_compl, isOpen_empty] #align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_isClopen theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) : diff --git a/Mathlib/Topology/ClopenBox.lean b/Mathlib/Topology/ClopenBox.lean index cfabbc59341ab..c6b70f5939cfe 100644 --- a/Mathlib/Topology/ClopenBox.lean +++ b/Mathlib/Topology/ClopenBox.lean @@ -37,7 +37,7 @@ theorem TopologicalSpace.Clopens.exists_prod_subset (W : Clopens (X × Y)) {a : ∃ U : Clopens X, a.1 ∈ U ∧ ∃ V : Clopens Y, a.2 ∈ V ∧ U ×ˢ V ≤ W := by have hp : Continuous (fun y : Y ↦ (a.1, y)) := Continuous.Prod.mk _ let V : Set Y := {y | (a.1, y) ∈ W} - have hV : IsCompact V := (W.2.2.preimage hp).isCompact + have hV : IsCompact V := (W.2.1.preimage hp).isCompact let U : Set X := {x | MapsTo (Prod.mk x) V W} have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2 exact ⟨⟨U, (ContinuousMap.isClopen_setOf_mapsTo hV W.2).preimage @@ -50,7 +50,7 @@ is a union of finitely many clopen boxes. -/ theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod (W : Clopens (X × Y)) : ∃ (I : Finset (Clopens X × Clopens Y)), W = I.sup fun i ↦ i.1 ×ˢ i.2 := by choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x) - rcases W.2.2.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦ + rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦ (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩ classical use I.image fun x ↦ (U x, V x) diff --git a/Mathlib/Topology/CompactOpen.lean b/Mathlib/Topology/CompactOpen.lean index 3c626072d3f32..a157820dba516 100644 --- a/Mathlib/Topology/CompactOpen.lean +++ b/Mathlib/Topology/CompactOpen.lean @@ -201,7 +201,7 @@ lemma isClosed_setOf_mapsTo {t : Set Y} (ht : IsClosed t) (s : Set X) : lemma isClopen_setOf_mapsTo (hK : IsCompact K) (hU : IsClopen U) : IsClopen {f : C(X, Y) | MapsTo f K U} := - ⟨isOpen_setOf_mapsTo hK hU.isOpen, isClosed_setOf_mapsTo hU.isClosed K⟩ + ⟨isClosed_setOf_mapsTo hU.isClosed K, isOpen_setOf_mapsTo hK hU.isOpen⟩ instance [T0Space Y] : T0Space C(X, Y) := t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index e3091aefd5805..adaaa7aa23683 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -861,7 +861,7 @@ theorem isClopen_iff [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = ⟨mt Or.inl h, mt (fun h2 => Or.inr <| (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩ let ⟨_, h2, h3⟩ := - nonempty_inter hs.1 hs.2.isOpen_compl (union_compl_self s) (nonempty_iff_ne_empty.2 h1.1) + nonempty_inter hs.2 hs.1.isOpen_compl (union_compl_self s) (nonempty_iff_ne_empty.2 h1.1) (nonempty_iff_ne_empty.2 h1.2) h3 h2, by rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]⟩ @@ -898,7 +898,7 @@ element. -/ lemma subsingleton_of_disjoint_isOpen_iUnion_eq_univ (h_open : ∀ i, IsOpen (s i)) (h_Union : ⋃ i, s i = univ) : Subsingleton ι := by - refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_open i, _⟩) + refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨_, h_open i⟩) rw [← isOpen_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff] refine' isOpen_iUnion (fun j ↦ _) rcases eq_or_ne i j with rfl | h_ne @@ -910,7 +910,7 @@ element. -/ lemma subsingleton_of_disjoint_isClosed_iUnion_eq_univ [Finite ι] (h_closed : ∀ i, IsClosed (s i)) (h_Union : ⋃ i, s i = univ) : Subsingleton ι := by - refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨_, h_closed i⟩) + refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_closed i, _⟩) rw [← isClosed_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff] refine' isClosed_iUnion_of_finite (fun j ↦ _) rcases eq_or_ne i j with rfl | h_ne @@ -956,14 +956,14 @@ lemma PreconnectedSpace.induction₂' [PreconnectedSpace α] (P : α → α → (h : ∀ x, ∀ᶠ y in 𝓝 x, P x y ∧ P y x) (h' : Transitive P) (x y : α) : P x y := by let u := {z | P x z} - have A : IsOpen u := by - apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_) - filter_upwards [h z] with t ht - exact h' hz ht.1 - have B : IsClosed u := by + have A : IsClosed u := by apply isClosed_iff_nhds.2 (fun z hz ↦ ?_) rcases hz _ (h z) with ⟨t, ht, h't⟩ exact h' h't ht.2 + have B : IsOpen u := by + apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_) + filter_upwards [h z] with t ht + exact h' hz ht.1 have C : u.Nonempty := ⟨x, (mem_of_mem_nhds (h x)).1⟩ have D : u = Set.univ := IsClopen.eq_univ ⟨A, B⟩ C show y ∈ u @@ -1317,9 +1317,9 @@ theorem isPreconnected_of_forall_constant {s : Set α} have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩ have : ContinuousOn u.boolIndicator s := by apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩ - · exact u_op.preimage continuous_subtype_val · rw [preimage_subtype_coe_eq_compl hsuv H] exact (v_op.preimage continuous_subtype_val).isClosed_compl + · exact u_op.preimage continuous_subtype_val simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.not_mem_iff_boolIndicator _).mp hy] using hs _ this x x_in_s y y_in_s #align is_preconnected_of_forall_constant isPreconnected_of_forall_constant diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean index 791840125b93f..c6ded2b9fd74d 100644 --- a/Mathlib/Topology/Connected/LocallyConnected.lean +++ b/Mathlib/Topology/Connected/LocallyConnected.lean @@ -83,7 +83,7 @@ theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} : theorem isClopen_connectedComponent [LocallyConnectedSpace α] {x : α} : IsClopen (connectedComponent x) := - ⟨isOpen_connectedComponent, isClosed_connectedComponent⟩ + ⟨isClosed_connectedComponent, isOpen_connectedComponent⟩ #align is_clopen_connected_component isClopen_connectedComponent theorem locallyConnectedSpace_iff_connectedComponentIn_open : diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean index f8dfba6c443a3..2b94b10bf4786 100644 --- a/Mathlib/Topology/Connected/PathConnected.lean +++ b/Mathlib/Topology/Connected/PathConnected.lean @@ -1276,17 +1276,17 @@ theorem pathConnectedSpace_iff_connectedSpace [LocPathConnectedSpace X] : rw [pathConnectedSpace_iff_eq] use Classical.arbitrary X refine' IsClopen.eq_univ ⟨_, _⟩ (by simp) + · rw [isClosed_iff_nhds] + intro y H + rcases (path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩ + rcases H U U_in with ⟨z, hz, hz'⟩ + exact (hU.joinedIn z hz y <| mem_of_mem_nhds U_in).joined.mem_pathComponent hz' · rw [isOpen_iff_mem_nhds] intro y y_in rcases (path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩ apply mem_of_superset U_in rw [← pathComponent_congr y_in] exact hU.subset_pathComponent (mem_of_mem_nhds U_in) - · rw [isClosed_iff_nhds] - intro y H - rcases (path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩ - rcases H U U_in with ⟨z, hz, hz'⟩ - exact (hU.joinedIn z hz y <| mem_of_mem_nhds U_in).joined.mem_pathComponent hz' #align path_connected_space_iff_connected_space pathConnectedSpace_iff_connectedSpace theorem pathConnected_subset_basis [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean index db4bc6f348fdb..40235d0cec856 100644 --- a/Mathlib/Topology/Connected/TotallyDisconnected.lean +++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean @@ -99,7 +99,7 @@ theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X] rcases h_contra with ⟨x, hx, y, hy, hxy⟩ obtain ⟨U, hU, hxU, hyU⟩ := hX hxy specialize - hS U Uᶜ hU.1 hU.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩ + hS U Uᶜ hU.2 hU.compl.2 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩ rw [inter_compl_self, Set.inter_empty] at hS exact Set.not_nonempty_empty hS #align is_totally_disconnected_of_clopen_set isTotallyDisconnected_of_isClopen_set diff --git a/Mathlib/Topology/DiscreteQuotient.lean b/Mathlib/Topology/DiscreteQuotient.lean index 15faff9e5518c..76eb6adb79bac 100644 --- a/Mathlib/Topology/DiscreteQuotient.lean +++ b/Mathlib/Topology/DiscreteQuotient.lean @@ -139,11 +139,11 @@ theorem isClopen_preimage (A : Set S) : IsClopen (S.proj ⁻¹' A) := #align discrete_quotient.is_clopen_preimage DiscreteQuotient.isClopen_preimage theorem isOpen_preimage (A : Set S) : IsOpen (S.proj ⁻¹' A) := - (S.isClopen_preimage A).1 + (S.isClopen_preimage A).2 #align discrete_quotient.is_open_preimage DiscreteQuotient.isOpen_preimage theorem isClosed_preimage (A : Set S) : IsClosed (S.proj ⁻¹' A) := - (S.isClopen_preimage A).2 + (S.isClopen_preimage A).1 #align discrete_quotient.is_closed_preimage DiscreteQuotient.isClosed_preimage theorem isClopen_setOf_rel (x : X) : IsClopen (setOf (S.Rel x)) := by diff --git a/Mathlib/Topology/LocallyConstant/Basic.lean b/Mathlib/Topology/LocallyConstant/Basic.lean index cff59267e784c..85636dd662c8c 100644 --- a/Mathlib/Topology/LocallyConstant/Basic.lean +++ b/Mathlib/Topology/LocallyConstant/Basic.lean @@ -74,7 +74,7 @@ theorem isClosed_fiber {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsClos #align is_locally_constant.is_closed_fiber IsLocallyConstant.isClosed_fiber theorem isClopen_fiber {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsClopen { x | f x = y } := - ⟨isOpen_fiber hf _, isClosed_fiber hf _⟩ + ⟨isClosed_fiber hf _, isOpen_fiber hf _⟩ #align is_locally_constant.is_clopen_fiber IsLocallyConstant.isClopen_fiber theorem iff_exists_open (f : X → Y) : @@ -339,13 +339,13 @@ def ofIsClopen {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x toFun x := if x ∈ U then 0 else 1 isLocallyConstant := by refine IsLocallyConstant.iff_isOpen_fiber.2 <| Fin.forall_fin_two.2 ⟨?_, ?_⟩ - · convert hU.1 using 1 + · convert hU.2 using 1 ext simp only [mem_singleton_iff, Fin.one_eq_zero_iff, mem_preimage, ite_eq_left_iff, Nat.succ_succ_ne_one] tauto · rw [← isClosed_compl_iff] - convert hU.2 + convert hU.1 ext simp #align locally_constant.of_clopen LocallyConstant.ofIsClopen diff --git a/Mathlib/Topology/SeparatedMap.lean b/Mathlib/Topology/SeparatedMap.lean index 7a443a1e101d2..ffbbf3f6356ac 100644 --- a/Mathlib/Topology/SeparatedMap.lean +++ b/Mathlib/Topology/SeparatedMap.lean @@ -195,7 +195,7 @@ variable (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) {s : Set A} (hs : then two lifts `g₁, g₂ : A → E` of a map `f : A → X` are equal if they agree at one point. -/ theorem eq_of_comp_eq [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂) (he : p ∘ g₁ = p ∘ g₂) (a : A) (ha : g₁ a = g₂ a) : g₁ = g₂ := funext fun a' ↦ by - apply (IsClopen.eq_univ ⟨inj.isOpen_eqLocus h₁ h₂ he, sep.isClosed_eqLocus h₁ h₂ he⟩ ⟨a, ha⟩).symm + apply (IsClopen.eq_univ ⟨sep.isClosed_eqLocus h₁ h₂ he, inj.isOpen_eqLocus h₁ h₂ he⟩ ⟨a, ha⟩).symm ▸ Set.mem_univ a' theorem eqOn_of_comp_eqOn (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s) diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 592769941c51f..92389bfba11cf 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -2108,7 +2108,7 @@ theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : -- that one of these closed sets must contain our whole thing. -- To reduce to the case where the cover is disjoint on all of `X` we need that `s` is closed have hs : @IsClosed X _ (⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s) := - isClosed_iInter fun s => s.2.1.2 + isClosed_iInter fun s => s.2.1.1 rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs] intro a b ha hb hab ab_disj -- Since our space is normal, we get two larger disjoint open sets containing the disjoint @@ -2121,7 +2121,7 @@ theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : `X` disjoint to it, but a finite intersection of clopen sets is clopen so we let this be our `s`. -/ · have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty - (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.2 + (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.1 rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1 cases' H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv) with si H2 @@ -2178,7 +2178,7 @@ theorem compact_t2_tot_disc_iff_tot_sep : TotallyDisconnectedSpace X ↔ Totally rw [connectedComponent_eq_iInter_isClopen, mem_iInter] rintro ⟨w : Set X, hw : IsClopen w, hy : y ∈ w⟩ by_contra hx - exact hyp wᶜ w hw.2.isOpen_compl hw.1 hx hy (@isCompl_compl _ w _).symm.codisjoint.top_le + exact hyp wᶜ w hw.1.isOpen_compl hw.2 hx hy (@isCompl_compl _ w _).symm.codisjoint.top_le disjoint_compl_left #align compact_t2_tot_disc_iff_tot_sep compact_t2_tot_disc_iff_tot_sep @@ -2199,7 +2199,7 @@ theorem nhds_basis_clopen (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s suffices : ∃ s : N, s.val ⊆ U · rcases this with ⟨⟨s, hs, hs'⟩, hs''⟩; exact ⟨s, ⟨hs', hs⟩, hs''⟩ haveI : Nonempty N := ⟨⟨univ, isClopen_univ, mem_univ x⟩⟩ - have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.2 + have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.1 have hdir : Directed Superset fun s : N => s.val := by rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩ exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left s t, inter_subset_right s t⟩ @@ -2207,13 +2207,13 @@ theorem nhds_basis_clopen (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s erw [hx, mem_singleton_iff] at y_in rwa [y_in] exact exists_subset_nhds_of_compactSpace hdir hNcl h_nhd - · rintro ⟨V, ⟨hxV, V_op, -⟩, hUV : V ⊆ U⟩ + · rintro ⟨V, ⟨hxV, -, V_op⟩, hUV : V ⊆ U⟩ rw [mem_nhds_iff] exact ⟨V, hUV, V_op, hxV⟩⟩ #align nhds_basis_clopen nhds_basis_clopen theorem isTopologicalBasis_isClopen : IsTopologicalBasis { s : Set X | IsClopen s } := by - apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.1 + apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.2 intro x U hxU U_op have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩ @@ -2237,7 +2237,7 @@ variable {H : Type*} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] /-- A locally compact Hausdorff totally disconnected space has a basis with clopen elements. -/ theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] : IsTopologicalBasis { s : Set H | IsClopen s } := by - refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.1) fun x U memU hU => ?_ + refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.2) fun x U memU hU => ?_ obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU let u : Set s := ((↑) : s → H) ⁻¹' interior s have u_open_in_s : IsOpen u := isOpen_interior.preimage continuous_subtype_val @@ -2245,7 +2245,7 @@ theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] : haveI : CompactSpace s := isCompact_iff_compactSpace.1 comp obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs have VisClopen' : IsClopen (((↑) : s → H) '' V) := by - refine' ⟨_, comp.isClosed.closedEmbedding_subtype_val.closed_iff_image_closed.1 VisClopen.2⟩ + refine' ⟨comp.isClosed.closedEmbedding_subtype_val.closed_iff_image_closed.1 VisClopen.1, _⟩ let v : Set u := ((↑) : u → s) ⁻¹' V have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl have f0 : Embedding ((↑) : u → H) := embedding_subtype_val.comp embedding_subtype_val @@ -2256,7 +2256,7 @@ theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] : apply Set.inter_eq_self_of_subset_left interior_subset rw [this] apply isOpen_interior - have f2 : IsOpen v := VisClopen.1.preimage continuous_subtype_val + have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_left V_sub] rw [f3] @@ -2292,7 +2292,7 @@ instance ConnectedComponents.t2 [T2Space X] [CompactSpace X] : T2Space (Connecte IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ (↑) ⁻¹' V = U := by have h := (isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed - _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.2) h + _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h cases' h with fin_a ha -- This clopen and its complement will separate the connected components of `a` and `b` set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i diff --git a/Mathlib/Topology/Sets/Compacts.lean b/Mathlib/Topology/Sets/Compacts.lean index 2d134ac88c176..2f3bd447d9862 100644 --- a/Mathlib/Topology/Sets/Compacts.lean +++ b/Mathlib/Topology/Sets/Compacts.lean @@ -484,7 +484,7 @@ def toOpens (s : CompactOpens α) : Opens α := ⟨s, s.isOpen⟩ /-- Reinterpret a compact open as a clopen. -/ @[simps] def toClopens [T2Space α] (s : CompactOpens α) : Clopens α := - ⟨s, s.isOpen, s.isCompact.isClosed⟩ + ⟨s, s.isCompact.isClosed, s.isOpen⟩ #align topological_space.compact_opens.to_clopens TopologicalSpace.CompactOpens.toClopens @[ext] diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean index 02bef1354b2c4..3f172281f2b28 100644 --- a/Mathlib/Topology/StoneCech.lean +++ b/Mathlib/Topology/StoneCech.lean @@ -98,7 +98,7 @@ instance : TotallyDisconnectedSpace (Ultrafilter α) := by intro s hs rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB let Z := { F : Ultrafilter α | s ∈ F } - have hZ : IsClopen Z := ⟨ultrafilter_isOpen_basic s, ultrafilter_isClosed_basic s⟩ + have hZ : IsClopen Z := ⟨ ultrafilter_isClosed_basic s, ultrafilter_isOpen_basic s⟩ exact hB ⟨Z, hZ, hs⟩ @[simp] theorem Ultrafilter.tendsto_pure_self (b : Ultrafilter α) : Tendsto pure b (𝓝 b) := by From d3d13f99611bf8a2cc07cd5011cd8760236d3dde Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 23 Jan 2024 15:34:49 -0800 Subject: [PATCH 2/3] two more files --- Mathlib/Topology/Category/Profinite/CofilteredLimit.lean | 6 +++--- Mathlib/Topology/Category/Stonean/Limits.lean | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean index 059599d20a7a2..d60b11045a56b 100644 --- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean +++ b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean @@ -65,7 +65,7 @@ theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsCl -- Porting note: `<;> continuity` fails -- Using this, since `U` is open, we can write `U` as a union of clopen sets all of which -- are preimages of clopens from the factors in the limit. - obtain ⟨S, hS, h⟩ := hB.open_eq_sUnion hU.1 + obtain ⟨S, hS, h⟩ := hB.open_eq_sUnion hU.2 clear hB let j : S → J := fun s => (hS s.2).choose let V : ∀ s : S, Set (F.obj (j s)) := fun s => (hS s.2).choose_spec.choose @@ -76,7 +76,7 @@ theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsCl -- clopens constructed in the previous step. have hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i) · intro s - exact (hV s).1.1.preimage (C.π.app (j s)).continuous + exact (hV s).1.2.preimage (C.π.app (j s)).continuous have hsU : U ⊆ ⋃ (i : ↑S), (fun s ↦ (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i · dsimp only rw [h] @@ -84,7 +84,7 @@ theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsCl refine' ⟨_, ⟨⟨T, hT⟩, rfl⟩, _⟩ dsimp only [forget_map_eq_coe] rwa [← (hV ⟨T, hT⟩).2] - have := hU.2.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU + have := hU.1.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU -- Porting note: same remark as after `hB` -- We thus obtain a finite set `G : Finset J` and a clopen set of `F.obj j` for each -- `j ∈ G` such that `U` is the union of the preimages of these clopen sets. diff --git a/Mathlib/Topology/Category/Stonean/Limits.lean b/Mathlib/Topology/Category/Stonean/Limits.lean index 8242e42902404..01632387d0ff5 100644 --- a/Mathlib/Topology/Category/Stonean/Limits.lean +++ b/Mathlib/Topology/Category/Stonean/Limits.lean @@ -182,14 +182,14 @@ def pullback : Stonean where dsimp at U have h : IsClopen (f ⁻¹' (Set.range i)) · constructor - · exact IsOpen.preimage f.continuous hi.open_range · refine' IsClosed.preimage f.continuous _ apply IsCompact.isClosed simp only [← Set.image_univ] exact IsCompact.image isCompact_univ i.continuous - have hU' : IsOpen (Subtype.val '' U) := h.1.openEmbedding_subtype_val.isOpenMap U hU + · exact IsOpen.preimage f.continuous hi.open_range + have hU' : IsOpen (Subtype.val '' U) := h.2.openEmbedding_subtype_val.isOpenMap U hU have := ExtremallyDisconnected.open_closure _ hU' - rw [h.2.closedEmbedding_subtype_val.closure_image_eq U] at this + rw [h.1.closedEmbedding_subtype_val.closure_image_eq U] at this suffices hhU : closure U = Subtype.val ⁻¹' (Subtype.val '' (closure U)) · rw [hhU] exact isOpen_induced this From 8bf8ed868a8d4f2a5c978d340cf4c8a34ce975a5 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 23 Jan 2024 21:28:25 -0800 Subject: [PATCH 3/3] fix Counterexamples --- Counterexamples/SorgenfreyLine.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean index 93c03f8b4cd2d..24469c7f45133 100644 --- a/Counterexamples/SorgenfreyLine.lean +++ b/Counterexamples/SorgenfreyLine.lean @@ -166,7 +166,7 @@ instance : ContinuousAdd ℝₗ := by exact (continuous_add.tendsto _).inf (MapsTo.tendsto fun x hx => add_le_add hx.1 hx.2) theorem isClopen_Ici (a : ℝₗ) : IsClopen (Ici a) := - ⟨isOpen_Ici a, isClosed_Ici⟩ + ⟨isClosed_Ici, isOpen_Ici a⟩ #align counterexample.sorgenfrey_line.is_clopen_Ici Counterexample.SorgenfreyLine.isClopen_Ici theorem isClopen_Iio (a : ℝₗ) : IsClopen (Iio a) := by @@ -247,7 +247,7 @@ theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ obtain rfl : x + y = c := by change (x, y) ∈ {p : ℝₗ × ℝₗ | p.1 + p.2 = c} exact closure_minimal (hs : s ⊆ {x | x.1 + x.2 = c}) (isClosed_antidiagonal c) H - rcases mem_closure_iff.1 H (Ici (x, y)) (isClopen_Ici_prod _).1 left_mem_Ici with + rcases mem_closure_iff.1 H (Ici (x, y)) (isClopen_Ici_prod _).2 left_mem_Ici with ⟨⟨x', y'⟩, ⟨hx : x ≤ x', hy : y ≤ y'⟩, H⟩ convert H · refine' hx.antisymm _