feat(Topology/Order): upgrade continuous_generateFrom to an iff (#…

…9259)

Similarly, upgrade `tendsto_nhds_generateFrom`, `IsTopologicalBasis.continuous`, `Topology.IsLower.continuous_of_Ici`, and `Topology.IsUpper.continuous_iff_Iic`.

The old lemmas are now deprecated, and the new ones have `_iff` in their names.
Once we remove the old lemmas, we can drop the `_iff` suffixes.

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -87,7 +87,7 @@ theorem toΓSpec_preim_basicOpen_eq (r : Γ.obj (op X)) :
 
 /-- `toΓSpecFun` is continuous. -/
 theorem toΓSpec_continuous : Continuous X.toΓSpecFun := by
-  apply isTopologicalBasis_basic_opens.continuous
+  rw [isTopologicalBasis_basic_opens.continuous_iff]
   rintro _ ⟨r, rfl⟩
   erw [X.toΓSpec_preim_basicOpen_eq r]
   exact (X.toRingedSpace.basicOpen r).2

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -334,7 +334,7 @@ open set in `Spec A⁰_f`.
 def toSpec {f : A} : (Proj.T| pbo f) ⟶ Spec.T A⁰_ f where
   toFun := ToSpec.toFun f
   continuous_toFun := by
-    apply IsTopologicalBasis.continuous PrimeSpectrum.isTopologicalBasis_basic_opens
+    rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]
     rintro _ ⟨⟨k, ⟨a, ha⟩, ⟨b, hb1⟩, ⟨k', hb2⟩⟩, rfl⟩; dsimp
     erw [ToSpec.preimage_eq f a b k ha hb1 ⟨k', hb2⟩]
     refine' isOpen_induced_iff.mpr ⟨(pbo f).1 ⊓ (pbo a).1, IsOpen.inter (pbo f).2 (pbo a).2, _⟩

Mathlib/Combinatorics/Hindman.lean

@@ -82,8 +82,8 @@ attribute [local instance] Ultrafilter.semigroup Ultrafilter.addSemigroup
 @[to_additive]
 theorem Ultrafilter.continuous_mul_left {M} [Semigroup M] (V : Ultrafilter M) :
     Continuous (· * V) :=
-  TopologicalSpace.IsTopologicalBasis.continuous ultrafilterBasis_is_basis _ <|
-    Set.forall_range_iff.mpr fun s => ultrafilter_isOpen_basic { m : M | ∀ᶠ m' in V, m * m' ∈ s }
+  ultrafilterBasis_is_basis.continuous_iff.2 <| Set.forall_range_iff.mpr fun s ↦
+    ultrafilter_isOpen_basic { m : M | ∀ᶠ m' in V, m * m' ∈ s }
 #align ultrafilter.continuous_mul_left Ultrafilter.continuous_mul_left
 #align ultrafilter.continuous_add_left Ultrafilter.continuous_add_left
 

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -338,7 +338,7 @@ theorem _root_.Measurable.exists_continuous {α β : Type*} [t : TopologicalSpac
     exists_polishSpace_forall_le T Tt Tpolish
   refine' ⟨t', t't, _, t'_polish⟩
   have : Continuous[t', _] (rangeFactorization f) :=
-    hb.continuous _ fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
+    hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
   exact continuous_subtype_val.comp this
 #align measurable.exists_continuous Measurable.exists_continuous
 

Mathlib/Topology/Algebra/Order/MonotoneContinuity.lean

@@ -303,9 +303,8 @@ variable {α β : Type*} [PartialOrder α] [PartialOrder β] [TopologicalSpace 
   [OrderTopology α] [OrderTopology β]
 
 protected theorem continuous (e : α ≃o β) : Continuous e := by
-  rw [‹OrderTopology β›.topology_eq_generate_intervals]
-  refine' continuous_generateFrom fun s hs => _
-  rcases hs with ⟨a, rfl | rfl⟩
+  rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]
+  rintro s ⟨a, rfl | rfl⟩
   · rw [e.preimage_Ioi]
     apply isOpen_lt'
   · rw [e.preimage_Iio]

Mathlib/Topology/Bases.lean

@@ -290,9 +290,15 @@ theorem isTopologicalBasis_of_cover {ι} {U : ι → Set α} (Uo : ∀ i, IsOpen
       image_subset_iff.2 hvu⟩
 #align topological_space.is_topological_basis_of_cover TopologicalSpace.isTopologicalBasis_of_cover
 
+protected theorem IsTopologicalBasis.continuous_iff {β : Type*} [TopologicalSpace β]
+    {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} :
+    Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s) := by
+  rw [hB.eq_generateFrom, continuous_generateFrom_iff]
+
+@[deprecated]
 protected theorem IsTopologicalBasis.continuous {β : Type*} [TopologicalSpace β] {B : Set (Set β)}
-    (hB : IsTopologicalBasis B) (f : α → β) (hf : ∀ s ∈ B, IsOpen (f ⁻¹' s)) : Continuous f := by
-  rw [hB.eq_generateFrom]; exact continuous_generateFrom hf
+    (hB : IsTopologicalBasis B) (f : α → β) (hf : ∀ s ∈ B, IsOpen (f ⁻¹' s)) : Continuous f :=
+  hB.continuous_iff.2 hf
 #align topological_space.is_topological_basis.continuous TopologicalSpace.IsTopologicalBasis.continuous
 
 variable (α)

Mathlib/Topology/CompactOpen.lean

@@ -103,7 +103,7 @@ private theorem preimage_gen {s : Set α} {u : Set γ} :
 
 /-- C(α, -) is a functor. -/
 theorem continuous_comp : Continuous (ContinuousMap.comp g : C(α, β) → C(α, γ)) :=
-  continuous_generateFrom fun m ⟨s, hs, u, hu, hm⟩ => by
+  continuous_generateFrom_iff.2 fun m ⟨s, hs, u, hu, hm⟩ => by
     rw [hm, preimage_gen g]; exact ContinuousMap.isOpen_gen hs (hu.preimage g.2)
 #align continuous_map.continuous_comp ContinuousMap.continuous_comp
 
@@ -129,7 +129,7 @@ private theorem image_gen {s : Set α} (_ : IsCompact s) {u : Set γ} (_ : IsOpe
 
 /-- C(-, γ) is a functor. -/
 theorem continuous_comp_left : Continuous (fun g => g.comp f : C(β, γ) → C(α, γ)) :=
-  continuous_generateFrom fun m ⟨s, hs, u, hu, hm⟩ => by
+  continuous_generateFrom_iff.2 fun m ⟨s, hs, u, hu, hm⟩ => by
     rw [hm, image_gen f hs hu]
     exact ContinuousMap.isOpen_gen (hs.image f.2) hu
 #align continuous_map.continuous_comp_left ContinuousMap.continuous_comp_left
@@ -138,7 +138,7 @@ theorem continuous_comp_left : Continuous (fun g => g.comp f : C(β, γ) → C(
   locally compact. This is Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's *Topologie Générale*. -/
 theorem continuous_comp' [LocallyCompactSpace β] :
     Continuous fun x : C(α, β) × C(β, γ) => x.2.comp x.1 :=
-  continuous_generateFrom
+  continuous_generateFrom_iff.2
     (by
       rintro M ⟨K, hK, U, hU, rfl⟩
       conv =>
@@ -338,7 +338,7 @@ theorem image_coev {y : β} (s : Set α) : coev α β y '' s = ({y} : Set β) ×
 
 -- The coevaluation map β → C(α, β × α) is continuous (always).
 theorem continuous_coev : Continuous (coev α β) :=
-  continuous_generateFrom <| by
+  continuous_generateFrom_iff.2 <| by
     rintro _ ⟨s, sc, u, uo, rfl⟩
     rw [isOpen_iff_forall_mem_open]
     intro y hy

Mathlib/Topology/Order.lean

@@ -81,8 +81,8 @@ theorem nhds_generateFrom {g : Set (Set α)} {a : α} :
     @nhds α (generateFrom g) a = ⨅ s ∈ { s | a ∈ s ∧ s ∈ g }, 𝓟 s := by
   letI := generateFrom g
   rw [nhds_def]
-  refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) ?_
-  refine le_iInf₂ fun s ⟨ha, hs⟩ => ?_; clear ‹s ∈ { s | a ∈ s ∧ IsOpen s }›
+  refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_
+  rintro s ⟨ha, hs⟩
   induction hs with
   | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
   | univ => exact le_top.trans_eq principal_univ.symm
@@ -92,10 +92,12 @@ theorem nhds_generateFrom {g : Set (Set α)} {a : α} :
     exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
 #align topological_space.nhds_generate_from TopologicalSpace.nhds_generateFrom
 
-theorem tendsto_nhds_generateFrom {β : Type*} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β}
-    (h : ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f) : Tendsto m f (@nhds β (generateFrom g) b) := by
-  rw [nhds_generateFrom]
-  exact tendsto_iInf.2 fun s => tendsto_iInf.2 fun ⟨hbs, hsg⟩ => tendsto_principal.2 <| h s hsg hbs
+lemma tendsto_nhds_generateFrom_iff {β : Type*} {m : α → β} {f : Filter α} {g : Set (Set β)}
+    {b : β} : Tendsto m f (@nhds β (generateFrom g) b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f := by
+  simp only [nhds_generateFrom, @forall_swap (b ∈ _), tendsto_iInf, mem_setOf_eq, and_imp,
+    tendsto_principal]; rfl
+
+@[deprecated] alias ⟨_, tendsto_nhds_generateFrom⟩ := tendsto_nhds_generateFrom_iff
 #align topological_space.tendsto_nhds_generate_from TopologicalSpace.tendsto_nhds_generateFrom
 
 /-- Construct a topology on α given the filter of neighborhoods of each point of α. -/
@@ -720,10 +722,11 @@ theorem continuous_iff_le_induced {t₁ : TopologicalSpace α} {t₂ : Topologic
   Iff.trans continuous_iff_coinduced_le (gc_coinduced_induced f _ _)
 #align continuous_iff_le_induced continuous_iff_le_induced
 
-theorem continuous_generateFrom {t : TopologicalSpace α} {b : Set (Set β)}
-    (h : ∀ s ∈ b, IsOpen (f ⁻¹' s)) :
-    Continuous[t, generateFrom b] f :=
-  continuous_iff_coinduced_le.2 <| le_generateFrom h
+lemma continuous_generateFrom_iff {t : TopologicalSpace α} {b : Set (Set β)} :
+    Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s) := by
+  rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]; rfl
+
+@[deprecated] alias ⟨_, continuous_generateFrom⟩ := continuous_generateFrom_iff
 #align continuous_generated_from continuous_generateFrom
 
 @[continuity]

Mathlib/Topology/Order/LowerUpperTopology.lean

@@ -277,16 +277,17 @@ protected theorem isTopologicalBasis : IsTopologicalBasis (lowerBasis α) := by
     exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩
 #align lower_topology.is_topological_basis Topology.IsLower.isTopologicalBasis
 
-/-- A function `f : β → α` with lower topology in the codomain is continuous provided that the
-preimage of every interval `Set.Ici a` is a closed set.
-
-TODO: upgrade to an `iff`. -/
-lemma continuous_of_Ici [TopologicalSpace β] {f : β → α} (h : ∀ a, IsClosed (f ⁻¹' (Ici a))) :
-    Continuous f := by
+/-- A function `f : β → α` with lower topology in the codomain is continuous
+if and only if the preimage of every interval `Set.Ici a` is a closed set.
+-/
+lemma continuous_iff_Ici [TopologicalSpace β] {f : β → α} :
+    Continuous f ↔ ∀ a, IsClosed (f ⁻¹' (Ici a)) := by
   obtain rfl := IsLower.topology_eq α
-  refine continuous_generateFrom ?_
-  rintro _ ⟨a, rfl⟩
-  exact (h a).isOpen_compl
+  simp [continuous_generateFrom_iff]
+
+/-- A function `f : β → α` with lower topology in the codomain is continuous provided that the
+preimage of every interval `Set.Ici a` is a closed set. -/
+@[deprecated] alias ⟨_, continuous_of_Ici⟩ := continuous_iff_Ici
 
 end Preorder
 
@@ -359,13 +360,18 @@ theorem closure_singleton (a : α) : closure {a} = Iic a :=
 protected theorem isTopologicalBasis : IsTopologicalBasis (upperBasis α) :=
   IsLower.isTopologicalBasis (α := αᵒᵈ)
 
-/-- A function `f : β → α` with upper topology in the codomain is continuous provided that the
-preimage of every interval `Set.Iic a` is a closed set.
+/-- A function `f : β → α` with upper topology in the codomain is continuous
+if and only if the preimage of every interval `Set.Iic a` is a closed set. -/
+lemma continuous_iff_Iic [TopologicalSpace β] {f : β → α} :
+    Continuous f ↔ ∀ a, IsClosed (f ⁻¹' (Iic a)) :=
+  IsLower.continuous_iff_Ici (α := αᵒᵈ)
 
-TODO: upgrade to an `iff`. -/
+/-- A function `f : β → α` with upper topology in the codomain is continuous
+provided that the preimage of every interval `Set.Iic a` is a closed set. -/
+@[deprecated]
 lemma continuous_of_Iic [TopologicalSpace β] {f : β → α} (h : ∀ a, IsClosed (f ⁻¹' (Iic a))) :
     Continuous f :=
-  IsLower.continuous_of_Ici (α := αᵒᵈ) h
+  continuous_iff_Iic.2 h
 
 end Preorder
 
@@ -416,7 +422,7 @@ variable [CompleteLattice α] [CompleteLattice β] [TopologicalSpace α] [IsLowe
   [TopologicalSpace β] [IsLower β]
 
 protected lemma _root_.sInfHom.continuous (f : sInfHom α β) : Continuous f := by
-  refine IsLower.continuous_of_Ici fun b => ?_
+  refine IsLower.continuous_iff_Ici.2 fun b => ?_
   convert isClosed_Ici (a := sInf <| f ⁻¹' Ici b)
   refine' Subset.antisymm (fun a => sInf_le) fun a ha => le_trans _ <|
     OrderHomClass.mono (f : α →o β) ha