Trigger CI for leanprover-community/batteries#1028

Mathlib.lean

@@ -4873,6 +4873,7 @@ import Mathlib.Topology.ContinuousMap.LocallyConstant
 import Mathlib.Topology.ContinuousMap.Ordered
 import Mathlib.Topology.ContinuousMap.Periodic
 import Mathlib.Topology.ContinuousMap.Polynomial
+import Mathlib.Topology.ContinuousMap.SecondCountableSpace
 import Mathlib.Topology.ContinuousMap.Sigma
 import Mathlib.Topology.ContinuousMap.Star
 import Mathlib.Topology.ContinuousMap.StarOrdered

Mathlib/RingTheory/AlgebraicIndependent.lean

@@ -3,10 +3,6 @@ Copyright (c) 2021 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.MvPolynomial.Equiv
-import Mathlib.Algebra.MvPolynomial.Supported
-import Mathlib.LinearAlgebra.LinearIndependent
-import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Algebraic
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.Data.Fin.Tuple.Reflection

Mathlib/Topology/Compactness/SigmaCompact.lean

@@ -368,6 +368,10 @@ theorem iUnion_eq : ⋃ n, K n = univ :=
 theorem exists_mem (x : X) : ∃ n, x ∈ K n :=
   iUnion_eq_univ_iff.1 K.iUnion_eq x
 
+theorem exists_mem_nhds (x : X) : ∃ n, K n ∈ 𝓝 x := by
+  rcases K.exists_mem x with ⟨n, hn⟩
+  exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩
+
 /-- A compact exhaustion eventually covers any compact set. -/
 theorem exists_superset_of_isCompact {s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n := by
   suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
@@ -422,7 +426,7 @@ noncomputable def choice (X : Type*) [TopologicalSpace X] [WeaklyLocallyCompactS
   · refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)
     exact iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩
 
-noncomputable instance [SigmaCompactSpace X] [LocallyCompactSpace X] :
+noncomputable instance [SigmaCompactSpace X] [WeaklyLocallyCompactSpace X] :
     Inhabited (CompactExhaustion X) :=
   ⟨CompactExhaustion.choice X⟩
 

Mathlib/Topology/ContinuousMap/SecondCountableSpace.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.CompactOpen
+
+/-!
+# Second countable topology on `C(X, Y)`
+
+In this file we prove that `C(X, Y)` with compact-open topology has second countable topology, if
+
+- both `X` and `Y` have second countable topology;
+- `X` is a locally compact space;
+-/
+
+open scoped Topology
+open Set Function Filter TopologicalSpace
+
+namespace ContinuousMap
+
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+
+theorem compactOpen_eq_generateFrom {S : Set (Set X)} {T : Set (Set Y)}
+    (hS₁ : ∀ K ∈ S, IsCompact K) (hT : IsTopologicalBasis T)
+    (hS₂ : ∀ f : C(X, Y), ∀ x, ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo f K V) :
+    compactOpen = .generateFrom (.image2 (fun K t ↦
+      {f : C(X, Y) | MapsTo f K (⋃₀ t)}) S {t : Set (Set Y) | t.Finite ∧ t ⊆ T}) := by
+  apply le_antisymm
+  · apply_rules [generateFrom_anti, image2_subset_iff.mpr]
+    intro K hK t ht
+    exact mem_image2_of_mem (hS₁ K hK) (isOpen_sUnion fun _ h ↦ hT.isOpen <| ht.2 h)
+  · refine le_of_nhds_le_nhds fun f ↦ ?_
+    simp only [nhds_compactOpen, le_iInf_iff, le_principal_iff]
+    intro K (hK : IsCompact K) U (hU : IsOpen U) hfKU
+    simp only [TopologicalSpace.nhds_generateFrom]
+    obtain ⟨t, htT, htf, hTU, hKT⟩ : ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ f '' K ⊆ ⋃₀ t := by
+      rw [hT.open_eq_sUnion' hU, mapsTo', sUnion_eq_biUnion] at hfKU
+      obtain ⟨t, ht, hfin, htK⟩ :=
+        (hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU
+      refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
+      rwa [sUnion_eq_biUnion]
+    rw [image_subset_iff] at hKT
+    obtain ⟨s, hsS, hsf, hKs, hst⟩ : ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo f (⋃₀ s) (⋃₀ t) := by
+      have : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo f L (⋃₀ t) := by
+        intro x hx
+        rcases hKT hx with ⟨V, hVt, hxV⟩
+        rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
+        exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
+      choose! L hLS hLmem hLt using this
+      rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩
+      refine ⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _,
+        by rwa [sUnion_image], ?_⟩
+      rw [mapsTo_sUnion, forall_mem_image]
+      exact fun x hx ↦ hLt x <| hsK x hx
+    have hsub : (⋂ L ∈ s, {g : C(X, Y) | MapsTo g L (⋃₀ t)}) ⊆ {g | MapsTo g K U} := by
+      simp only [← setOf_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]
+      exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)
+    refine mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub
+    refine mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_principal_self _
+    exact ⟨hst.mono_left (subset_sUnion_of_mem hL), mem_image2_of_mem (hsS hL) ⟨htf, htT⟩⟩
+
+/-- A version of `instSecondCountableTopology` with a technical assumption
+instead of `[SecondCountableTopology X] [LocallyCompactSpace X]`.
+It is here as a reminder of what could be an intermediate goal,
+if someone tries to weaken the assumptions in the instance
+(e.g., from `[LocallyCompactSpace X]` to `[LocallyCompactPair X Y]` - not sure if it's true). -/
+theorem secondCountableTopology [SecondCountableTopology Y]
+    (hX : ∃ S : Set (Set X), S.Countable ∧ (∀ K ∈ S, IsCompact K) ∧
+      ∀ f : C(X, Y), ∀ V, IsOpen V → ∀ x ∈ f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo f K V) :
+    SecondCountableTopology C(X, Y) where
+  is_open_generated_countable := by
+    rcases hX with ⟨S, hScount, hScomp, hS⟩
+    refine ⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩
+    · exact .image2 hScount (countable_setOf_finite_subset (countable_countableBasis Y)) _
+    · intro f x V hV hx
+      apply hS
+      exacts [isOpen_of_mem_countableBasis hV, hx]
+
+instance instSecondCountableTopology [SecondCountableTopology X] [LocallyCompactSpace X]
+    [SecondCountableTopology Y] : SecondCountableTopology C(X, Y) := by
+  apply secondCountableTopology
+  have (U : countableBasis X) : LocallyCompactSpace U.1 :=
+    (isOpen_of_mem_countableBasis U.2).locallyCompactSpace
+  set K := fun U : countableBasis X ↦ CompactExhaustion.choice U.1
+  use ⋃ U : countableBasis X, Set.range fun n ↦ K U n
+  refine ⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩
+  · simp only [mem_iUnion, mem_range]
+    rintro K ⟨U, n, rfl⟩
+    exact ((K U).isCompact _).image continuous_subtype_val
+  · intro f V hVo x hxV
+    obtain ⟨U, hU, hxU, hUV⟩ : ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ f ⁻¹' V := by
+      rw [← (isBasis_countableBasis _).mem_nhds_iff]
+      exact (hVo.preimage (map_continuous f)).mem_nhds hxV
+    lift x to U using hxU
+    lift U to countableBasis X using hU
+    rcases (K U).exists_mem_nhds x with ⟨n, hn⟩
+    refine ⟨K U n, mem_iUnion.2 ⟨U, mem_range_self _⟩, ?_, ?_⟩
+    · rw [← map_nhds_subtype_coe_eq_nhds x.2]
+      exacts [image_mem_map hn, (isOpen_of_mem_countableBasis U.2).mem_nhds x.2]
+    · rw [mapsTo_image_iff]
+      exact fun y _ ↦ hUV y.2
+
+instance instSeparableSpace [SecondCountableTopology X] [LocallyCompactSpace X]
+    [SecondCountableTopology Y] : SeparableSpace C(X, Y) :=
+  inferInstance
+
+end ContinuousMap

Mathlib/Topology/Instances/Discrete.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.Order.SuccPred.Basic
 import Mathlib.Topology.Order.Basic
 
 /-!
@@ -42,70 +41,25 @@ theorem DiscreteTopology.secondCountableTopology_of_encodable {α : Type*}
     [TopologicalSpace α] [DiscreteTopology α] [Countable α] : SecondCountableTopology α :=
   DiscreteTopology.secondCountableTopology_of_countable
 
-theorem bot_topologicalSpace_eq_generateFrom_of_pred_succOrder {α} [LinearOrder α] [PredOrder α]
-    [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] :
-    (⊥ : TopologicalSpace α) = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a } := by
-  refine (eq_bot_of_singletons_open fun a => ?_).symm
-  have h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a) := by
-    suffices h_singleton_eq_inter' : {a} = Iic a ∩ Ici a by
-      rw [h_singleton_eq_inter', ← Ioi_pred, ← Iio_succ]
-    rw [inter_comm, Ici_inter_Iic, Icc_self a]
-  rw [h_singleton_eq_inter]
-  letI := Preorder.topology α
-  apply IsOpen.inter
-  · exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
-  · exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
-
-theorem discreteTopology_iff_orderTopology_of_pred_succ' [LinearOrder α] [PredOrder α]
-    [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : DiscreteTopology α ↔ OrderTopology α := by
-  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-  · rw [h.eq_bot]
-    exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder
-  · rw [h.topology_eq_generate_intervals]
-    exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder.symm
-
-instance (priority := 100) DiscreteTopology.orderTopology_of_pred_succ' [h : DiscreteTopology α]
-    [LinearOrder α] [PredOrder α] [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : OrderTopology α :=
-  discreteTopology_iff_orderTopology_of_pred_succ'.1 h
-
 theorem LinearOrder.bot_topologicalSpace_eq_generateFrom {α} [LinearOrder α] [PredOrder α]
     [SuccOrder α] : (⊥ : TopologicalSpace α) = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a } := by
-  refine (eq_bot_of_singletons_open fun a => ?_).symm
-  have h_singleton_eq_inter : {a} = Iic a ∩ Ici a := by rw [inter_comm, Ici_inter_Iic, Icc_self a]
-  by_cases ha_top : IsTop a
-  · rw [ha_top.Iic_eq, inter_comm, inter_univ] at h_singleton_eq_inter
-    by_cases ha_bot : IsBot a
-    · rw [ha_bot.Ici_eq] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      -- Porting note: Specified instance for `isOpen_univ` explicitly to fix an error.
-      apply @isOpen_univ _ (generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a })
-    · rw [isBot_iff_isMin] at ha_bot
-      rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
-  · rw [isTop_iff_isMax] at ha_top
-    rw [← Iio_succ_of_not_isMax ha_top] at h_singleton_eq_inter
-    by_cases ha_bot : IsBot a
-    · rw [ha_bot.Ici_eq, inter_univ] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
-    · rw [isBot_iff_isMin] at ha_bot
-      rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      -- Porting note: Specified instance for `IsOpen.inter` explicitly to fix an error.
-      letI := Preorder.topology α
-      apply IsOpen.inter
-      · exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
-      · exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
+  let _ := Preorder.topology α
+  have : OrderTopology α := ⟨rfl⟩
+  exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm
+
+@[deprecated (since := "2024-11-02")]
+alias bot_topologicalSpace_eq_generateFrom_of_pred_succOrder :=
+  LinearOrder.bot_topologicalSpace_eq_generateFrom
 
 theorem discreteTopology_iff_orderTopology_of_pred_succ [LinearOrder α] [PredOrder α]
     [SuccOrder α] : DiscreteTopology α ↔ OrderTopology α := by
-  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-  · rw [h.eq_bot]
-    exact LinearOrder.bot_topologicalSpace_eq_generateFrom
-  · rw [h.topology_eq_generate_intervals]
-    exact LinearOrder.bot_topologicalSpace_eq_generateFrom.symm
+  refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
+  rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_generateFrom]
+
+@[deprecated (since := "2024-11-02")]
+alias discreteTopology_iff_orderTopology_of_pred_succ' :=
+  discreteTopology_iff_orderTopology_of_pred_succ
 
-instance (priority := 100) DiscreteTopology.orderTopology_of_pred_succ [h : DiscreteTopology α]
-    [LinearOrder α] [PredOrder α] [SuccOrder α] : OrderTopology α :=
-  discreteTopology_iff_orderTopology_of_pred_succ.mp h
+instance OrderTopology.of_discreteTopology [LinearOrder α] [PredOrder α] [SuccOrder α]
+    [DiscreteTopology α] : OrderTopology α :=
+  discreteTopology_iff_orderTopology_of_pred_succ.mp ‹_›

Mathlib/Topology/Order.lean

@@ -185,7 +185,7 @@ def gciGenerateFrom (α : Type*) :
   topology whose open sets are those sets open in every member of the collection. -/
 instance : CompleteLattice (TopologicalSpace α) := (gciGenerateFrom α).liftCompleteLattice
 
-@[mono]
+@[mono, gcongr]
 theorem generateFrom_anti {α} {g₁ g₂ : Set (Set α)} (h : g₁ ⊆ g₂) :
     generateFrom g₂ ≤ generateFrom g₁ :=
   (gc_generateFrom _).monotone_u h

Mathlib/Topology/Order/OrderClosed.lean

@@ -237,12 +237,16 @@ theorem Ioo_mem_nhdsWithin_Iio' (H : a < b) : Ioo a b ∈ 𝓝[<] b := by
 theorem Ioo_mem_nhdsWithin_Iio (H : b ∈ Ioc a c) : Ioo a c ∈ 𝓝[<] b :=
   mem_of_superset (Ioo_mem_nhdsWithin_Iio' H.1) <| Ioo_subset_Ioo_right H.2
 
-theorem CovBy.nhdsWithin_Iio (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
+protected theorem CovBy.nhdsWithin_Iio (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
   empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Iio' h.1
 
+protected theorem PredOrder.nhdsWithin_Iio [PredOrder α] : 𝓝[<] a = ⊥ := by
+  if h : IsMin a then simp [h.Iio_eq]
+  else exact (Order.pred_covBy_of_not_isMin h).nhdsWithin_Iio
+
 theorem Ico_mem_nhdsWithin_Iio (H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b :=
   mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Ico_self
--- Porting note (#11215): TODO: swap `'`?
+
 -- Porting note (#11215): TODO: swap `'`?
 theorem Ico_mem_nhdsWithin_Iio' (H : a < b) : Ico a b ∈ 𝓝[<] b :=
   Ico_mem_nhdsWithin_Iio ⟨H, le_rfl⟩
@@ -282,6 +286,12 @@ theorem continuousWithinAt_Ioo_iff_Iio (h : a < b) :
 #### Point included
 -/
 
+protected theorem CovBy.nhdsWithin_Iic (H : a ⋖ b) : 𝓝[≤] b = pure b := by
+  rw [← Iio_insert, nhdsWithin_insert, H.nhdsWithin_Iio, sup_bot_eq]
+
+protected theorem PredOrder.nhdsWithin_Iic [PredOrder α] : 𝓝[≤] b = pure b := by
+  rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsWithin_Iio, sup_bot_eq]
+
 theorem Ioc_mem_nhdsWithin_Iic' (H : a < b) : Ioc a b ∈ 𝓝[≤] b :=
   inter_mem (nhdsWithin_le_nhds <| Ioi_mem_nhds H) self_mem_nhdsWithin
 
@@ -446,9 +456,12 @@ theorem Ioo_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioo a c ∈ 
 theorem Ioo_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[>] a :=
   Ioo_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩
 
-theorem CovBy.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ :=
+protected theorem CovBy.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ :=
   empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Ioi' h.1
 
+protected theorem SuccOrder.nhdsWithin_Ioi [SuccOrder α] : 𝓝[>] a = ⊥ :=
+  PredOrder.nhdsWithin_Iio (α := αᵒᵈ)
+
 theorem Ioc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b :=
   mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Ioc_self
 
@@ -492,6 +505,12 @@ theorem continuousWithinAt_Ioo_iff_Ioi (h : a < b) :
 ### Point included
 -/
 
+protected theorem CovBy.nhdsWithin_Ici (H : a ⋖ b) : 𝓝[≥] a = pure a :=
+  H.toDual.nhdsWithin_Iic
+
+protected theorem SuccOrder.nhdsWithin_Ici [SuccOrder α] : 𝓝[≥] a = pure a :=
+  PredOrder.nhdsWithin_Iic (α := αᵒᵈ)
+
 theorem Ico_mem_nhdsWithin_Ici' (H : a < b) : Ico a b ∈ 𝓝[≥] a :=
   inter_mem_nhdsWithin _ <| Iio_mem_nhds H
 
@@ -666,7 +685,17 @@ theorem Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x
 theorem Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x :=
   mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self
 
-variable [TopologicalSpace γ]
+/-- The only order closed topology on a linear order which is a `PredOrder` and a `SuccOrder`
+is the discrete topology.
+
+This theorem is not an instance,
+because it causes searches for `PredOrder` and `SuccOrder` with their `Preorder` arguments
+and very rarely matches. -/
+theorem DiscreteTopology.of_predOrder_succOrder [PredOrder α] [SuccOrder α] :
+    DiscreteTopology α := by
+  refine discreteTopology_iff_nhds.mpr fun a ↦ ?_
+  rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsWithin_Iic,
+    SuccOrder.nhdsWithin_Ioi, sup_bot_eq]
 
 end LinearOrder
 

Mathlib/Topology/Separation/Basic.lean

@@ -1225,7 +1225,7 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i,
 theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds
     {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X}
     {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ 𝓝 (f x)) (hKc : IsCompact K)
-    (hKx : K ∈ 𝓝 x) : ∃ K ∈ 𝓝 x, IsCompact K ∧ MapsTo f K s := by
+    (hKx : K ∈ 𝓝 x) : ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s := by
   have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior
   obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by
     simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c13ced73d98ffe9a3bdffc65da5f5139f4bbc095",
+   "rev": "1a3fe2e8e46f0ceb8ea084a5596a1d5f6fb90883",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "batteries-docs",