From 20c7b4b802f5ad61a2c1621e707b906cfe79366c Mon Sep 17 00:00:00 2001 From: grunweg Date: Fri, 26 Jan 2024 03:44:15 +0000 Subject: [PATCH] chore(Topology/Basic): re-use variables; rename a : X to x : X (#9993) Co-authored-by: sgouezel Co-authored-by: Yury G. Kudryashov --- .../Asymptotics/AsymptoticEquivalent.lean | 4 +- Mathlib/Analysis/Calculus/FDeriv/Basic.lean | 2 +- .../Fourier/RiemannLebesgueLemma.lean | 2 +- .../InnerProductSpace/Projection.lean | 4 +- .../NormedSpace/Multilinear/Basic.lean | 2 +- .../SpecialFunctions/Pow/Asymptotics.lean | 2 +- Mathlib/Topology/Algebra/Algebra.lean | 2 +- .../Topology/Algebra/Order/LiminfLimsup.lean | 2 +- Mathlib/Topology/Bases.lean | 2 +- Mathlib/Topology/Basic.lean | 625 +++++++++--------- .../Topology/Category/Profinite/Nobeling.lean | 4 +- .../MetricSpace/HausdorffDistance.lean | 2 +- Mathlib/Topology/Order.lean | 8 +- Mathlib/Topology/UniformSpace/Basic.lean | 4 +- .../UniformSpace/CompactConvergence.lean | 2 +- 15 files changed, 334 insertions(+), 333 deletions(-) diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean index 0b0be0a42cc75..5777dc7dfce62 100644 --- a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean +++ b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean @@ -141,10 +141,10 @@ theorem isEquivalent_const_iff_tendsto {c : Ξ²} (h : c β‰  0) : u ~[l] const _ c ↔ Tendsto u l (𝓝 c) := by simp (config := { unfoldPartialApp := true }) only [IsEquivalent, const, isLittleO_const_iff h] constructor <;> intro h - Β· have := h.sub (tendsto_const_nhds (a := -c)) + Β· have := h.sub (tendsto_const_nhds (x := -c)) simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this exact this - Β· have := h.sub (tendsto_const_nhds (a := c)) + Β· have := h.sub (tendsto_const_nhds (x := c)) rwa [sub_self] at this #align asymptotics.is_equivalent_const_iff_tendsto Asymptotics.isEquivalent_const_iff_tendsto diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean index 07f0a64f66c6f..37a1eb26eb2e3 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean @@ -779,7 +779,7 @@ theorem HasFDerivAtFilter.tendsto_nhds (hL : L ≀ 𝓝 x) (h : HasFDerivAtFilte refine' h.isBigO_sub.trans_tendsto (Tendsto.mono_left _ hL) rw [← sub_self x] exact tendsto_id.sub tendsto_const_nhds - have := this.add (@tendsto_const_nhds _ _ _ (f x) _) + have := this.add (tendsto_const_nhds (x := f x)) rw [zero_add (f x)] at this exact this.congr (by simp only [sub_add_cancel, eq_self_iff_true, forall_const]) #align has_fderiv_at_filter.tendsto_nhds HasFDerivAtFilter.tendsto_nhds diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index 484fe3d9a954b..aac5de6aca3bb 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -216,7 +216,7 @@ variable (f) theorem tendsto_integral_exp_inner_smul_cocompact : Tendsto (fun w : V => ∫ v, e[-βŸͺv, w⟫] β€’ f v) (cocompact V) (𝓝 0) := by by_cases hfi : Integrable f; swap - Β· convert tendsto_const_nhds (a := (0 : E)) with w + Β· convert tendsto_const_nhds (x := (0 : E)) with w apply integral_undef rwa [← fourier_integrand_integrable w] refine' Metric.tendsto_nhds.mpr fun Ξ΅ hΞ΅ => _ diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 99a809497aa8e..9deb69d19b52d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -172,10 +172,10 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h convert this exact sqrt_zero.symm have eq₁ : Tendsto (fun n : β„• => 8 * Ξ΄ * (1 / (n + 1))) atTop (nhds (0 : ℝ)) := by - convert (@tendsto_const_nhds _ _ _ (8 * Ξ΄) _).mul tendsto_one_div_add_atTop_nhds_0_nat + convert (tendsto_const_nhds (x := 8 * Ξ΄)).mul tendsto_one_div_add_atTop_nhds_0_nat simp only [mul_zero] have : Tendsto (fun n : β„• => (4 : ℝ) * (1 / (n + 1))) atTop (nhds (0 : ℝ)) := by - convert (@tendsto_const_nhds _ _ _ (4 : ℝ) _).mul tendsto_one_div_add_atTop_nhds_0_nat + convert (tendsto_const_nhds (x := 4)).mul tendsto_one_div_add_atTop_nhds_0_nat simp only [mul_zero] have eqβ‚‚ : Tendsto (fun n : β„• => (4 : ℝ) * (1 / (n + 1)) * (1 / (n + 1))) atTop (nhds (0 : ℝ)) := by diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean index 750baf3b15b28..a089b2ee9d4d4 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean @@ -1311,7 +1311,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM map_smul' := fun v i c x => by skip have A := hF (Function.update v i (c β€’ x)) - have B := Filter.Tendsto.smul (@tendsto_const_nhds _ β„• _ c _) (hF (Function.update v i x)) + have B := Filter.Tendsto.smul (tendsto_const_nhds (x := c)) (hF (Function.update v i x)) simp? at A B says simp only [map_smul] at A B exact tendsto_nhds_unique A B } -- and that `F` has norm at most `(b 0 + β€–f 0β€–)`. diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean index 32f4903d0b9c2..e61eeb0ee68c3 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean @@ -108,7 +108,7 @@ theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 β‰  b) : ((tendsto_exp_nhds_0_nhds_1.comp (by simpa only [mul_zero, pow_one] using - (@tendsto_const_nhds _ _ _ a _).mul + (tendsto_const_nhds (x := a)).mul (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp tendsto_log_atTop) apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean index 525009986330a..296ec961e072e 100644 --- a/Mathlib/Topology/Algebra/Algebra.lean +++ b/Mathlib/Topology/Algebra/Algebra.lean @@ -111,7 +111,7 @@ theorem Subalgebra.le_topologicalClosure (s : Subalgebra R A) : s ≀ s.topologi #align subalgebra.le_topological_closure Subalgebra.le_topologicalClosure theorem Subalgebra.isClosed_topologicalClosure (s : Subalgebra R A) : - IsClosed (s.topologicalClosure : Set A) := by convert @isClosed_closure A _ s + IsClosed (s.topologicalClosure : Set A) := by convert @isClosed_closure A s _ #align subalgebra.is_closed_topological_closure Subalgebra.isClosed_topologicalClosure theorem Subalgebra.topologicalClosure_minimal (s : Subalgebra R A) {t : Subalgebra R A} (h : s ≀ t) diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean index 6fc5d651befad..600b8f90b9733 100644 --- a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean +++ b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean @@ -183,7 +183,7 @@ set_option linter.uppercaseLean3 false in theorem limsSup_nhds (a : Ξ±) : limsSup (𝓝 a) = a := csInf_eq_of_forall_ge_of_forall_gt_exists_lt (isBounded_le_nhds a) - (fun a' (h : { n : Ξ± | n ≀ a' } ∈ 𝓝 a) ↦ show a ≀ a' from @mem_of_mem_nhds Ξ± _ a _ h) + (fun a' (h : { n : Ξ± | n ≀ a' } ∈ 𝓝 a) ↦ show a ≀ a' from @mem_of_mem_nhds Ξ± a _ _ h) fun b (hba : a < b) ↦ show βˆƒ c, { n : Ξ± | n ≀ c } ∈ 𝓝 a ∧ c < b from match dense_or_discrete a b with diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index 4d64a0a400e79..4a533a5444355 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -130,7 +130,7 @@ theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set Ξ±)} (h_open : βˆ€ u rcases h_nhds a univ trivial isOpen_univ with ⟨u, h₁, hβ‚‚, -⟩ exact ⟨u, h₁, hβ‚‚βŸ© Β· refine' (le_generateFrom h_open).antisymm fun u hu => _ - refine' (@isOpen_iff_nhds Ξ± (generateFrom s) u).mpr fun a ha => _ + refine (@isOpen_iff_nhds Ξ± u (generateFrom s)).mpr fun a ha ↦ ?_ rcases h_nhds a u ha hu with ⟨v, hvs, hav, hvu⟩ rw [nhds_generateFrom] exact iInfβ‚‚_le_of_le v ⟨hav, hvs⟩ (le_principal_iff.2 hvu) diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index e5317295169b5..64a4f72dbbd2d 100644 --- a/Mathlib/Topology/Basic.lean +++ b/Mathlib/Topology/Basic.lean @@ -20,8 +20,8 @@ Then `Set X` gets predicates `IsOpen`, `IsClosed` and functions `interior`, `clo along `F : Filter Ξ±` if `MapClusterPt x F f : ClusterPt x (map f F)`. In particular the notion of cluster point of a sequence `u` is `MapClusterPt x atTop u`. -For topological spaces `X` and `Y`, a function `f : X β†’ Y` and a point `a : X`, -`ContinuousAt f a` means `f` is continuous at `a`, and global continuity is +For topological spaces `X` and `Y`, a function `f : X β†’ Y` and a point `x : X`, +`ContinuousAt f x` means `f` is continuous at `x`, and global continuity is `Continuous f`. There is also a version of continuity `PContinuous` for partially defined functions. @@ -93,7 +93,7 @@ def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : βˆ… section TopologicalSpace variable {X : Type u} {Y : Type v} {ΞΉ : Sort w} {Ξ± Ξ² : Type*} - {a : X} {s s₁ sβ‚‚ t : Set X} {p p₁ pβ‚‚ : X β†’ Prop} + {x : X} {s s₁ sβ‚‚ t : Set X} {p p₁ pβ‚‚ : X β†’ Prop} /-- `IsOpen s` means that `s` is open in the ambient topological space on `X` -/ def IsOpen [TopologicalSpace X] : Set X β†’ Prop := TopologicalSpace.IsOpen @@ -105,7 +105,7 @@ scoped[Topology] notation (name := IsOpen_of) "IsOpen[" t "]" => @IsOpen _ t open Topology -lemma isOpen_mk {p h₁ hβ‚‚ h₃} {s : Set X} : IsOpen[⟨p, h₁, hβ‚‚, hβ‚ƒβŸ©] s ↔ p s := Iff.rfl +lemma isOpen_mk {p h₁ hβ‚‚ h₃} : IsOpen[⟨p, h₁, hβ‚‚, hβ‚ƒβŸ©] s ↔ p s := Iff.rfl #align is_open_mk isOpen_mk @[ext] @@ -136,7 +136,7 @@ protected theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace X} : ⟨fun h s => h β–Έ Iff.rfl, fun h => by ext; exact h _⟩ #align topological_space_eq_iff TopologicalSpace.ext_iff -theorem isOpen_fold {s : Set X} {t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s := +theorem isOpen_fold {t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s := rfl #align is_open_fold isOpen_fold @@ -189,10 +189,10 @@ theorem isOpen_biInter_finset {s : Finset Ξ±} {f : Ξ± β†’ Set X} (h : βˆ€ i ∈ #align is_open_bInter_finset isOpen_biInter_finset @[simp] -- porting note: added `simp` -theorem isOpen_const {p : Prop} : IsOpen { _a : X | p } := by by_cases p <;> simp [*] +theorem isOpen_const {p : Prop} : IsOpen { _x : X | p } := by by_cases p <;> simp [*] #align is_open_const isOpen_const -theorem IsOpen.and : IsOpen { a | p₁ a } β†’ IsOpen { a | pβ‚‚ a } β†’ IsOpen { a | p₁ a ∧ pβ‚‚ a } := +theorem IsOpen.and : IsOpen { x | p₁ x } β†’ IsOpen { x | pβ‚‚ x } β†’ IsOpen { x | p₁ x ∧ pβ‚‚ x } := IsOpen.inter #align is_open.and IsOpen.and @@ -206,19 +206,19 @@ set_option quotPrecheck false in /-- Notation for `IsClosed` with respect to a non-standard topology. -/ scoped[Topology] notation (name := IsClosed_of) "IsClosed[" t "]" => @IsClosed _ t -@[simp] theorem isOpen_compl_iff {s : Set X} : IsOpen sᢜ ↔ IsClosed s := +@[simp] theorem isOpen_compl_iff : IsOpen sᢜ ↔ IsClosed s := ⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩ #align is_open_compl_iff isOpen_compl_iff theorem TopologicalSpace.ext_iff_isClosed {t₁ tβ‚‚ : TopologicalSpace X} : t₁ = tβ‚‚ ↔ βˆ€ s, IsClosed[t₁] s ↔ IsClosed[tβ‚‚] s := by rw [TopologicalSpace.ext_iff, compl_surjective.forall] - simp only [@isOpen_compl_iff _ t₁, @isOpen_compl_iff _ tβ‚‚] + simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ tβ‚‚] alias ⟨_, TopologicalSpace.ext_isClosed⟩ := TopologicalSpace.ext_iff_isClosed -- porting note: new lemma -theorem isClosed_const {p : Prop} : IsClosed { _a : X | p } := ⟨isOpen_const (p := Β¬p)⟩ +theorem isClosed_const {p : Prop} : IsClosed { _x : X | p } := ⟨isOpen_const (p := Β¬p)⟩ @[simp] theorem isClosed_empty : IsClosed (βˆ… : Set X) := isClosed_const #align is_closed_empty isClosed_empty @@ -251,7 +251,7 @@ theorem isClosed_compl_iff {s : Set X} : IsClosed sᢜ ↔ IsOpen s := by alias ⟨_, IsOpen.isClosed_compl⟩ := isClosed_compl_iff #align is_open.is_closed_compl IsOpen.isClosed_compl -theorem IsOpen.sdiff {s t : Set X} (h₁ : IsOpen s) (hβ‚‚ : IsClosed t) : IsOpen (s \ t) := +theorem IsOpen.sdiff (h₁ : IsOpen s) (hβ‚‚ : IsClosed t) : IsOpen (s \ t) := IsOpen.inter h₁ hβ‚‚.isOpen_compl #align is_open.sdiff IsOpen.sdiff @@ -261,7 +261,7 @@ theorem IsClosed.inter (h₁ : IsClosed s₁) (hβ‚‚ : IsClosed sβ‚‚) : IsClosed exact IsOpen.union h₁ hβ‚‚ #align is_closed.inter IsClosed.inter -theorem IsClosed.sdiff {s t : Set X} (h₁ : IsClosed s) (hβ‚‚ : IsOpen t) : IsClosed (s \ t) := +theorem IsClosed.sdiff (h₁ : IsClosed s) (hβ‚‚ : IsOpen t) : IsClosed (s \ t) := IsClosed.inter h₁ (isClosed_compl_iff.mpr hβ‚‚) #align is_closed.sdiff IsClosed.sdiff @@ -301,40 +301,40 @@ def interior (s : Set X) : Set X := #align interior interior -- porting note: use `βˆƒ t, t βŠ† s ∧ _` instead of `βˆƒ t βŠ† s, _` -theorem mem_interior {s : Set X} {x : X} : x ∈ interior s ↔ βˆƒ t, t βŠ† s ∧ IsOpen t ∧ x ∈ t := by +theorem mem_interior : x ∈ interior s ↔ βˆƒ t, t βŠ† s ∧ IsOpen t ∧ x ∈ t := by simp only [interior, mem_sUnion, mem_setOf_eq, and_assoc, and_left_comm] #align mem_interior mem_interiorβ‚“ @[simp] -theorem isOpen_interior {s : Set X} : IsOpen (interior s) := +theorem isOpen_interior : IsOpen (interior s) := isOpen_sUnion fun _ => And.left #align is_open_interior isOpen_interior -theorem interior_subset {s : Set X} : interior s βŠ† s := +theorem interior_subset : interior s βŠ† s := sUnion_subset fun _ => And.right #align interior_subset interior_subset -theorem interior_maximal {s t : Set X} (h₁ : t βŠ† s) (hβ‚‚ : IsOpen t) : t βŠ† interior s := +theorem interior_maximal (h₁ : t βŠ† s) (hβ‚‚ : IsOpen t) : t βŠ† interior s := subset_sUnion_of_mem ⟨hβ‚‚, hβ‚βŸ© #align interior_maximal interior_maximal -theorem IsOpen.interior_eq {s : Set X} (h : IsOpen s) : interior s = s := +theorem IsOpen.interior_eq (h : IsOpen s) : interior s = s := interior_subset.antisymm (interior_maximal (Subset.refl s) h) #align is_open.interior_eq IsOpen.interior_eq -theorem interior_eq_iff_isOpen {s : Set X} : interior s = s ↔ IsOpen s := +theorem interior_eq_iff_isOpen : interior s = s ↔ IsOpen s := ⟨fun h => h β–Έ isOpen_interior, IsOpen.interior_eq⟩ #align interior_eq_iff_is_open interior_eq_iff_isOpen -theorem subset_interior_iff_isOpen {s : Set X} : s βŠ† interior s ↔ IsOpen s := by +theorem subset_interior_iff_isOpen : s βŠ† interior s ↔ IsOpen s := by simp only [interior_eq_iff_isOpen.symm, Subset.antisymm_iff, interior_subset, true_and] #align subset_interior_iff_is_open subset_interior_iff_isOpen -theorem IsOpen.subset_interior_iff {s t : Set X} (h₁ : IsOpen s) : s βŠ† interior t ↔ s βŠ† t := +theorem IsOpen.subset_interior_iff (h₁ : IsOpen s) : s βŠ† interior t ↔ s βŠ† t := ⟨fun h => Subset.trans h interior_subset, fun hβ‚‚ => interior_maximal hβ‚‚ hβ‚βŸ© #align is_open.subset_interior_iff IsOpen.subset_interior_iff -theorem subset_interior_iff {s t : Set X} : t βŠ† interior s ↔ βˆƒ U, IsOpen U ∧ t βŠ† U ∧ U βŠ† s := +theorem subset_interior_iff : t βŠ† interior s ↔ βˆƒ U, IsOpen U ∧ t βŠ† U ∧ U βŠ† s := ⟨fun h => ⟨interior s, isOpen_interior, h, interior_subset⟩, fun ⟨_U, hU, htU, hUs⟩ => htU.trans (interior_maximal hUs hU)⟩ #align subset_interior_iff subset_interior_iff @@ -343,7 +343,7 @@ lemma interior_subset_iff : interior s βŠ† t ↔ βˆ€ U, IsOpen U β†’ U βŠ† s β†’ simp [interior] @[mono] -theorem interior_mono {s t : Set X} (h : s βŠ† t) : interior s βŠ† interior t := +theorem interior_mono (h : s βŠ† t) : interior s βŠ† interior t := interior_maximal (Subset.trans interior_subset h) isOpen_interior #align interior_mono interior_mono @@ -358,17 +358,17 @@ theorem interior_univ : interior (univ : Set X) = univ := #align interior_univ interior_univ @[simp] -theorem interior_eq_univ {s : Set X} : interior s = univ ↔ s = univ := +theorem interior_eq_univ : interior s = univ ↔ s = univ := ⟨fun h => univ_subset_iff.mp <| h.symm.trans_le interior_subset, fun h => h.symm β–Έ interior_univ⟩ #align interior_eq_univ interior_eq_univ @[simp] -theorem interior_interior {s : Set X} : interior (interior s) = interior s := +theorem interior_interior : interior (interior s) = interior s := isOpen_interior.interior_eq #align interior_interior interior_interior @[simp] -theorem interior_inter {s t : Set X} : interior (s ∩ t) = interior s ∩ interior t := +theorem interior_inter : interior (s ∩ t) = interior s ∩ interior t := (Monotone.map_inf_le (fun _ _ ↦ interior_mono) s t).antisymm <| interior_maximal (inter_subset_inter interior_subset interior_subset) <| isOpen_interior.inter isOpen_interior @@ -394,7 +394,7 @@ theorem interior_iInter_of_finite [Finite ΞΉ] (f : ΞΉ β†’ Set X) : rw [← sInter_range, (finite_range f).interior_sInter, biInter_range] #align interior_Inter interior_iInter_of_finite -theorem interior_union_isClosed_of_interior_empty {s t : Set X} (h₁ : IsClosed s) +theorem interior_union_isClosed_of_interior_empty (h₁ : IsClosed s) (hβ‚‚ : interior t = βˆ…) : interior (s βˆͺ t) = interior s := have : interior (s βˆͺ t) βŠ† s := fun x ⟨u, ⟨(hu₁ : IsOpen u), (huβ‚‚ : u βŠ† s βˆͺ t)⟩, (hx₁ : x ∈ u)⟩ => by_contradiction fun hxβ‚‚ : x βˆ‰ s => @@ -440,51 +440,51 @@ set_option quotPrecheck false in scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t @[simp] -theorem isClosed_closure {s : Set X} : IsClosed (closure s) := +theorem isClosed_closure : IsClosed (closure s) := isClosed_sInter fun _ => And.left #align is_closed_closure isClosed_closure -theorem subset_closure {s : Set X} : s βŠ† closure s := +theorem subset_closure : s βŠ† closure s := subset_sInter fun _ => And.right #align subset_closure subset_closure -theorem not_mem_of_not_mem_closure {s : Set X} {P : X} (hP : P βˆ‰ closure s) : P βˆ‰ s := fun h => +theorem not_mem_of_not_mem_closure {P : X} (hP : P βˆ‰ closure s) : P βˆ‰ s := fun h => hP (subset_closure h) #align not_mem_of_not_mem_closure not_mem_of_not_mem_closure -theorem closure_minimal {s t : Set X} (h₁ : s βŠ† t) (hβ‚‚ : IsClosed t) : closure s βŠ† t := +theorem closure_minimal (h₁ : s βŠ† t) (hβ‚‚ : IsClosed t) : closure s βŠ† t := sInter_subset_of_mem ⟨hβ‚‚, hβ‚βŸ© #align closure_minimal closure_minimal -theorem Disjoint.closure_left {s t : Set X} (hd : Disjoint s t) (ht : IsOpen t) : +theorem Disjoint.closure_left (hd : Disjoint s t) (ht : IsOpen t) : Disjoint (closure s) t := disjoint_compl_left.mono_left <| closure_minimal hd.subset_compl_right ht.isClosed_compl #align disjoint.closure_left Disjoint.closure_left -theorem Disjoint.closure_right {s t : Set X} (hd : Disjoint s t) (hs : IsOpen s) : +theorem Disjoint.closure_right (hd : Disjoint s t) (hs : IsOpen s) : Disjoint s (closure t) := (hd.symm.closure_left hs).symm #align disjoint.closure_right Disjoint.closure_right -theorem IsClosed.closure_eq {s : Set X} (h : IsClosed s) : closure s = s := +theorem IsClosed.closure_eq (h : IsClosed s) : closure s = s := Subset.antisymm (closure_minimal (Subset.refl s) h) subset_closure #align is_closed.closure_eq IsClosed.closure_eq -theorem IsClosed.closure_subset {s : Set X} (hs : IsClosed s) : closure s βŠ† s := +theorem IsClosed.closure_subset (hs : IsClosed s) : closure s βŠ† s := closure_minimal (Subset.refl _) hs #align is_closed.closure_subset IsClosed.closure_subset -theorem IsClosed.closure_subset_iff {s t : Set X} (h₁ : IsClosed t) : closure s βŠ† t ↔ s βŠ† t := +theorem IsClosed.closure_subset_iff (h₁ : IsClosed t) : closure s βŠ† t ↔ s βŠ† t := ⟨Subset.trans subset_closure, fun h => closure_minimal h hβ‚βŸ© #align is_closed.closure_subset_iff IsClosed.closure_subset_iff -theorem IsClosed.mem_iff_closure_subset {s : Set X} (hs : IsClosed s) {x : X} : +theorem IsClosed.mem_iff_closure_subset (hs : IsClosed s) : x ∈ s ↔ closure ({x} : Set X) βŠ† s := (hs.closure_subset_iff.trans Set.singleton_subset_iff).symm #align is_closed.mem_iff_closure_subset IsClosed.mem_iff_closure_subset @[mono] -theorem closure_mono {s t : Set X} (h : s βŠ† t) : closure s βŠ† closure t := +theorem closure_mono (h : s βŠ† t) : closure s βŠ† closure t := closure_minimal (Subset.trans h subset_closure) isClosed_closure #align closure_mono closure_mono @@ -492,7 +492,7 @@ theorem monotone_closure (X : Type*) [TopologicalSpace X] : Monotone (@closure X closure_mono #align monotone_closure monotone_closure -theorem diff_subset_closure_iff {s t : Set X} : s \ t βŠ† closure t ↔ s βŠ† closure t := by +theorem diff_subset_closure_iff : s \ t βŠ† closure t ↔ s βŠ† closure t := by rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure] #align diff_subset_closure_iff diff_subset_closure_iff @@ -501,15 +501,15 @@ theorem closure_inter_subset_inter_closure (s t : Set X) : (monotone_closure X).map_inf_le s t #align closure_inter_subset_inter_closure closure_inter_subset_inter_closure -theorem isClosed_of_closure_subset {s : Set X} (h : closure s βŠ† s) : IsClosed s := by +theorem isClosed_of_closure_subset (h : closure s βŠ† s) : IsClosed s := by rw [subset_closure.antisymm h]; exact isClosed_closure #align is_closed_of_closure_subset isClosed_of_closure_subset -theorem closure_eq_iff_isClosed {s : Set X} : closure s = s ↔ IsClosed s := +theorem closure_eq_iff_isClosed : closure s = s ↔ IsClosed s := ⟨fun h => h β–Έ isClosed_closure, IsClosed.closure_eq⟩ #align closure_eq_iff_is_closed closure_eq_iff_isClosed -theorem closure_subset_iff_isClosed {s : Set X} : closure s βŠ† s ↔ IsClosed s := +theorem closure_subset_iff_isClosed : closure s βŠ† s ↔ IsClosed s := ⟨isClosed_of_closure_subset, IsClosed.closure_subset⟩ #align closure_subset_iff_is_closed closure_subset_iff_isClosed @@ -524,7 +524,7 @@ theorem closure_empty_iff (s : Set X) : closure s = βˆ… ↔ s = βˆ… := #align closure_empty_iff closure_empty_iff @[simp] -theorem closure_nonempty_iff {s : Set X} : (closure s).Nonempty ↔ s.Nonempty := by +theorem closure_nonempty_iff : (closure s).Nonempty ↔ s.Nonempty := by simp only [nonempty_iff_ne_empty, Ne.def, closure_empty_iff] #align closure_nonempty_iff closure_nonempty_iff @@ -538,17 +538,17 @@ theorem closure_univ : closure (univ : Set X) = univ := #align closure_univ closure_univ @[simp] -theorem closure_closure {s : Set X} : closure (closure s) = closure s := +theorem closure_closure : closure (closure s) = closure s := isClosed_closure.closure_eq #align closure_closure closure_closure -theorem closure_eq_compl_interior_compl {s : Set X} : closure s = (interior sᢜ)ᢜ := by +theorem closure_eq_compl_interior_compl : closure s = (interior sᢜ)ᢜ := by rw [interior, closure, compl_sUnion, compl_image_set_of] simp only [compl_subset_compl, isOpen_compl_iff] #align closure_eq_compl_interior_compl closure_eq_compl_interior_compl @[simp] -theorem closure_union {s t : Set X} : closure (s βˆͺ t) = closure s βˆͺ closure t := by +theorem closure_union : closure (s βˆͺ t) = closure s βˆͺ closure t := by simp [closure_eq_compl_interior_compl, compl_inter] #align closure_union closure_union @@ -572,22 +572,22 @@ theorem closure_iUnion_of_finite [Finite ΞΉ] (f : ΞΉ β†’ Set X) : rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range] #align closure_Union closure_iUnion_of_finite -theorem interior_subset_closure {s : Set X} : interior s βŠ† closure s := +theorem interior_subset_closure : interior s βŠ† closure s := Subset.trans interior_subset subset_closure #align interior_subset_closure interior_subset_closure @[simp] -theorem interior_compl {s : Set X} : interior sᢜ = (closure s)ᢜ := by +theorem interior_compl : interior sᢜ = (closure s)ᢜ := by simp [closure_eq_compl_interior_compl] #align interior_compl interior_compl @[simp] -theorem closure_compl {s : Set X} : closure sᢜ = (interior s)ᢜ := by +theorem closure_compl : closure sᢜ = (interior s)ᢜ := by simp [closure_eq_compl_interior_compl] #align closure_compl closure_compl -theorem mem_closure_iff {s : Set X} {a : X} : - a ∈ closure s ↔ βˆ€ o, IsOpen o β†’ a ∈ o β†’ (o ∩ s).Nonempty := +theorem mem_closure_iff : + x ∈ closure s ↔ βˆ€ o, IsOpen o β†’ x ∈ o β†’ (o ∩ s).Nonempty := ⟨fun h o oo ao => by_contradiction fun os => have : s βŠ† oᢜ := fun x xs xo => os ⟨x, xo, xs⟩ @@ -598,7 +598,7 @@ theorem mem_closure_iff {s : Set X} {a : X} : hc (hβ‚‚ hs)⟩ #align mem_closure_iff mem_closure_iff -theorem closure_inter_open_nonempty_iff {s t : Set X} (h : IsOpen t) : +theorem closure_inter_open_nonempty_iff (h : IsOpen t) : (closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty := ⟨fun ⟨_x, hxcs, hxt⟩ => inter_comm t s β–Έ mem_closure_iff.1 hxcs t h hxt, fun h => h.mono <| inf_le_inf_right t subset_closure⟩ @@ -630,24 +630,24 @@ def Dense (s : Set X) : Prop := βˆ€ x, x ∈ closure s #align dense Dense -theorem dense_iff_closure_eq {s : Set X} : Dense s ↔ closure s = univ := +theorem dense_iff_closure_eq : Dense s ↔ closure s = univ := eq_univ_iff_forall.symm #align dense_iff_closure_eq dense_iff_closure_eq alias ⟨Dense.closure_eq, _⟩ := dense_iff_closure_eq #align dense.closure_eq Dense.closure_eq -theorem interior_eq_empty_iff_dense_compl {s : Set X} : interior s = βˆ… ↔ Dense sᢜ := by +theorem interior_eq_empty_iff_dense_compl : interior s = βˆ… ↔ Dense sᢜ := by rw [dense_iff_closure_eq, closure_compl, compl_univ_iff] #align interior_eq_empty_iff_dense_compl interior_eq_empty_iff_dense_compl -theorem Dense.interior_compl {s : Set X} (h : Dense s) : interior sᢜ = βˆ… := +theorem Dense.interior_compl (h : Dense s) : interior sᢜ = βˆ… := interior_eq_empty_iff_dense_compl.2 <| by rwa [compl_compl] #align dense.interior_compl Dense.interior_compl /-- The closure of a set `s` is dense if and only if `s` is dense. -/ @[simp] -theorem dense_closure {s : Set X} : Dense (closure s) ↔ Dense s := by +theorem dense_closure : Dense (closure s) ↔ Dense s := by rw [Dense, Dense, closure_closure] #align dense_closure dense_closure @@ -661,7 +661,7 @@ theorem dense_univ : Dense (univ : Set X) := fun _ => subset_closure trivial #align dense_univ dense_univ /-- A set is dense if and only if it has a nonempty intersection with each nonempty open set. -/ -theorem dense_iff_inter_open {s : Set X} : +theorem dense_iff_inter_open : Dense s ↔ βˆ€ U, IsOpen U β†’ U.Nonempty β†’ (U ∩ s).Nonempty := by constructor <;> intro h Β· rintro U U_op ⟨x, x_in⟩ @@ -675,29 +675,29 @@ theorem dense_iff_inter_open {s : Set X} : alias ⟨Dense.inter_open_nonempty, _⟩ := dense_iff_inter_open #align dense.inter_open_nonempty Dense.inter_open_nonempty -theorem Dense.exists_mem_open {s : Set X} (hs : Dense s) {U : Set X} (ho : IsOpen U) +theorem Dense.exists_mem_open (hs : Dense s) {U : Set X} (ho : IsOpen U) (hne : U.Nonempty) : βˆƒ x ∈ s, x ∈ U := let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne ⟨x, hx.2, hx.1⟩ #align dense.exists_mem_open Dense.exists_mem_open -theorem Dense.nonempty_iff {s : Set X} (hs : Dense s) : s.Nonempty ↔ Nonempty X := +theorem Dense.nonempty_iff (hs : Dense s) : s.Nonempty ↔ Nonempty X := ⟨fun ⟨x, _⟩ => ⟨x⟩, fun ⟨x⟩ => let ⟨y, hy⟩ := hs.inter_open_nonempty _ isOpen_univ ⟨x, trivial⟩ ⟨y, hy.2⟩⟩ #align dense.nonempty_iff Dense.nonempty_iff -theorem Dense.nonempty [h : Nonempty X] {s : Set X} (hs : Dense s) : s.Nonempty := +theorem Dense.nonempty [h : Nonempty X] (hs : Dense s) : s.Nonempty := hs.nonempty_iff.2 h #align dense.nonempty Dense.nonempty @[mono] -theorem Dense.mono {s₁ sβ‚‚ : Set X} (h : s₁ βŠ† sβ‚‚) (hd : Dense s₁) : Dense sβ‚‚ := fun x => +theorem Dense.mono (h : s₁ βŠ† sβ‚‚) (hd : Dense s₁) : Dense sβ‚‚ := fun x => closure_mono h (hd x) #align dense.mono Dense.mono /-- Complement to a singleton is dense if and only if the singleton is not an open set. -/ -theorem dense_compl_singleton_iff_not_open {x : X} : +theorem dense_compl_singleton_iff_not_open : Dense ({x}ᢜ : Set X) ↔ Β¬IsOpen ({x} : Set X) := by constructor Β· intro hd ho @@ -738,11 +738,11 @@ theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s := by inter_eq_self_of_subset_right interior_subset, empty_union] #align self_diff_frontier self_diff_frontier -theorem frontier_eq_closure_inter_closure {s : Set X} : frontier s = closure s ∩ closure sᢜ := by +theorem frontier_eq_closure_inter_closure : frontier s = closure s ∩ closure sᢜ := by rw [closure_compl, frontier, diff_eq] #align frontier_eq_closure_inter_closure frontier_eq_closure_inter_closure -theorem frontier_subset_closure {s : Set X} : frontier s βŠ† closure s := +theorem frontier_subset_closure : frontier s βŠ† closure s := diff_subset _ _ #align frontier_subset_closure frontier_subset_closure @@ -750,11 +750,11 @@ theorem IsClosed.frontier_subset (hs : IsClosed s) : frontier s βŠ† s := frontier_subset_closure.trans hs.closure_eq.subset #align is_closed.frontier_subset IsClosed.frontier_subset -theorem frontier_closure_subset {s : Set X} : frontier (closure s) βŠ† frontier s := +theorem frontier_closure_subset : frontier (closure s) βŠ† frontier s := diff_subset_diff closure_closure.subset <| interior_mono subset_closure #align frontier_closure_subset frontier_closure_subset -theorem frontier_interior_subset {s : Set X} : frontier (interior s) βŠ† frontier s := +theorem frontier_interior_subset : frontier (interior s) βŠ† frontier s := diff_subset_diff (closure_mono interior_subset) interior_interior.symm.subset #align frontier_interior_subset frontier_interior_subset @@ -784,25 +784,25 @@ theorem frontier_union_subset (s t : Set X) : simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᢜ tᢜ #align frontier_union_subset frontier_union_subset -theorem IsClosed.frontier_eq {s : Set X} (hs : IsClosed s) : frontier s = s \ interior s := by +theorem IsClosed.frontier_eq (hs : IsClosed s) : frontier s = s \ interior s := by rw [frontier, hs.closure_eq] #align is_closed.frontier_eq IsClosed.frontier_eq -theorem IsOpen.frontier_eq {s : Set X} (hs : IsOpen s) : frontier s = closure s \ s := by +theorem IsOpen.frontier_eq (hs : IsOpen s) : frontier s = closure s \ s := by rw [frontier, hs.interior_eq] #align is_open.frontier_eq IsOpen.frontier_eq -theorem IsOpen.inter_frontier_eq {s : Set X} (hs : IsOpen s) : s ∩ frontier s = βˆ… := by +theorem IsOpen.inter_frontier_eq (hs : IsOpen s) : s ∩ frontier s = βˆ… := by rw [hs.frontier_eq, inter_diff_self] #align is_open.inter_frontier_eq IsOpen.inter_frontier_eq /-- The frontier of a set is closed. -/ -theorem isClosed_frontier {s : Set X} : IsClosed (frontier s) := by +theorem isClosed_frontier : IsClosed (frontier s) := by rw [frontier_eq_closure_inter_closure]; exact IsClosed.inter isClosed_closure isClosed_closure #align is_closed_frontier isClosed_frontier /-- The frontier of a closed set has no interior point. -/ -theorem interior_frontier {s : Set X} (h : IsClosed s) : interior (frontier s) = βˆ… := by +theorem interior_frontier (h : IsClosed s) : interior (frontier s) = βˆ… := by have A : frontier s = s \ interior s := h.frontier_eq have B : interior (frontier s) βŠ† interior s := by rw [A]; exact interior_mono (diff_subset _ _) have C : interior (frontier s) βŠ† frontier s := interior_subset @@ -828,12 +828,12 @@ theorem Disjoint.frontier_right (hs : IsOpen s) (hd : Disjoint s t) : Disjoint s (hd.symm.frontier_left hs).symm #align disjoint.frontier_right Disjoint.frontier_right -theorem frontier_eq_inter_compl_interior {s : Set X} : +theorem frontier_eq_inter_compl_interior : frontier s = (interior s)ᢜ ∩ (interior sᢜ)ᢜ := by rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior] #align frontier_eq_inter_compl_interior frontier_eq_inter_compl_interior -theorem compl_frontier_eq_union_interior {s : Set X} : +theorem compl_frontier_eq_union_interior : (frontier s)ᢜ = interior s βˆͺ interior sᢜ := by rw [frontier_eq_inter_compl_interior] simp only [compl_inter, compl_compl] @@ -843,18 +843,18 @@ theorem compl_frontier_eq_union_interior {s : Set X} : ### Neighborhoods -/ -/-- A set is called a neighborhood of `a` if it contains an open set around `a`. The set of all -neighborhoods of `a` forms a filter, the neighborhood filter at `a`, is here defined as the -infimum over the principal filters of all open sets containing `a`. -/ -irreducible_def nhds (a : X) : Filter X := - β¨… s ∈ { s : Set X | a ∈ s ∧ IsOpen s }, π“Ÿ s +/-- A set is called a neighborhood of `x` if it contains an open set around `x`. The set of all +neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the +infimum over the principal filters of all open sets containing `x`. -/ +irreducible_def nhds (x : X) : Filter X := + β¨… s ∈ { s : Set X | x ∈ s ∧ IsOpen s }, π“Ÿ s #align nhds nhds #align nhds_def nhds_def -/-- The "neighborhood within" filter. Elements of `𝓝[s] a` are sets containing the -intersection of `s` and a neighborhood of `a`. -/ -def nhdsWithin (a : X) (s : Set X) : Filter X := - nhds a βŠ“ π“Ÿ s +/-- The "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the +intersection of `s` and a neighborhood of `x`. -/ +def nhdsWithin (x : X) (s : Set X) : Filter X := + nhds x βŠ“ π“Ÿ s #align nhds_within nhdsWithin section @@ -882,164 +882,164 @@ scoped[Topology] notation3 "𝓝[<] " x:100 => nhdsWithin x (Set.Iio x) end -theorem nhds_def' (a : X) : 𝓝 a = β¨… (s : Set X) (_ : IsOpen s) (_ : a ∈ s), π“Ÿ s := by - simp only [nhds_def, mem_setOf_eq, @and_comm (a ∈ _), iInf_and] +theorem nhds_def' (x : X) : 𝓝 x = β¨… (s : Set X) (_ : IsOpen s) (_ : x ∈ s), π“Ÿ s := by + simp only [nhds_def, mem_setOf_eq, @and_comm (x ∈ _), iInf_and] #align nhds_def' nhds_def' -/-- The open sets containing `a` are a basis for the neighborhood filter. See `nhds_basis_opens'` +/-- The open sets containing `x` are a basis for the neighborhood filter. See `nhds_basis_opens'` for a variant using open neighborhoods instead. -/ -theorem nhds_basis_opens (a : X) : - (𝓝 a).HasBasis (fun s : Set X => a ∈ s ∧ IsOpen s) fun s => s := by +theorem nhds_basis_opens (x : X) : + (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ IsOpen s) fun s => s := by rw [nhds_def] exact hasBasis_biInf_principal (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ => ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left _ _, inter_subset_right _ _⟩⟩) - ⟨univ, ⟨mem_univ a, isOpen_univ⟩⟩ + ⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩ #align nhds_basis_opens nhds_basis_opens -theorem nhds_basis_closeds (a : X) : (𝓝 a).HasBasis (fun s : Set X => a βˆ‰ s ∧ IsClosed s) compl := - ⟨fun t => (nhds_basis_opens a).mem_iff.trans <| +theorem nhds_basis_closeds (x : X) : (𝓝 x).HasBasis (fun s : Set X => x βˆ‰ s ∧ IsClosed s) compl := + ⟨fun t => (nhds_basis_opens x).mem_iff.trans <| compl_surjective.exists.trans <| by simp only [isOpen_compl_iff, mem_compl_iff]⟩ #align nhds_basis_closeds nhds_basis_closeds -/-- A filter lies below the neighborhood filter at `a` iff it contains every open set around `a`. -/ -theorem le_nhds_iff {f a} : f ≀ 𝓝 a ↔ βˆ€ s : Set X, a ∈ s β†’ IsOpen s β†’ s ∈ f := by simp [nhds_def] +/-- A filter lies below the neighborhood filter at `x` iff it contains every open set around `x`. -/ +theorem le_nhds_iff {f} : f ≀ 𝓝 x ↔ βˆ€ s : Set X, x ∈ s β†’ IsOpen s β†’ s ∈ f := by simp [nhds_def] #align le_nhds_iff le_nhds_iff -/-- To show a filter is above the neighborhood filter at `a`, it suffices to show that it is above -the principal filter of some open set `s` containing `a`. -/ -theorem nhds_le_of_le {f a} {s : Set X} (h : a ∈ s) (o : IsOpen s) (sf : π“Ÿ s ≀ f) : 𝓝 a ≀ f := by +/-- To show a filter is above the neighborhood filter at `x`, it suffices to show that it is above +the principal filter of some open set `s` containing `x`. -/ +theorem nhds_le_of_le {f} (h : x ∈ s) (o : IsOpen s) (sf : π“Ÿ s ≀ f) : 𝓝 x ≀ f := by rw [nhds_def]; exact iInfβ‚‚_le_of_le s ⟨h, o⟩ sf #align nhds_le_of_le nhds_le_of_le -- porting note: use `βˆƒ t, t βŠ† s ∧ _` instead of `βˆƒ t βŠ† s, _` -theorem mem_nhds_iff {a : X} {s : Set X} : s ∈ 𝓝 a ↔ βˆƒ t, t βŠ† s ∧ IsOpen t ∧ a ∈ t := - (nhds_basis_opens a).mem_iff.trans <| exists_congr fun _ => +theorem mem_nhds_iff : s ∈ 𝓝 x ↔ βˆƒ t, t βŠ† s ∧ IsOpen t ∧ x ∈ t := + (nhds_basis_opens x).mem_iff.trans <| exists_congr fun _ => ⟨fun h => ⟨h.2, h.1.2, h.1.1⟩, fun h => ⟨⟨h.2.2, h.2.1⟩, h.1⟩⟩ #align mem_nhds_iff mem_nhds_iffβ‚“ -/-- A predicate is true in a neighborhood of `a` iff it is true for all the points in an open set -containing `a`. -/ -theorem eventually_nhds_iff {a : X} {p : X β†’ Prop} : - (βˆ€αΆ  x in 𝓝 a, p x) ↔ βˆƒ t : Set X, (βˆ€ x ∈ t, p x) ∧ IsOpen t ∧ a ∈ t := +/-- A predicate is true in a neighborhood of `x` iff it is true for all the points in an open set +containing `x`. -/ +theorem eventually_nhds_iff {p : X β†’ Prop} : + (βˆ€αΆ  x in 𝓝 x, p x) ↔ βˆƒ t : Set X, (βˆ€ x ∈ t, p x) ∧ IsOpen t ∧ x ∈ t := mem_nhds_iff.trans <| by simp only [subset_def, exists_prop, mem_setOf_eq] #align eventually_nhds_iff eventually_nhds_iff -theorem mem_interior_iff_mem_nhds {s : Set X} {a : X} : a ∈ interior s ↔ s ∈ 𝓝 a := +theorem mem_interior_iff_mem_nhds : x ∈ interior s ↔ s ∈ 𝓝 x := mem_interior.trans mem_nhds_iff.symm #align mem_interior_iff_mem_nhds mem_interior_iff_mem_nhds -theorem map_nhds {a : X} {f : X β†’ Ξ±} : - map f (𝓝 a) = β¨… s ∈ { s : Set X | a ∈ s ∧ IsOpen s }, π“Ÿ (f '' s) := - ((nhds_basis_opens a).map f).eq_biInf +theorem map_nhds {f : X β†’ Ξ±} : + map f (𝓝 x) = β¨… s ∈ { s : Set X | x ∈ s ∧ IsOpen s }, π“Ÿ (f '' s) := + ((nhds_basis_opens x).map f).eq_biInf #align map_nhds map_nhds -theorem mem_of_mem_nhds {a : X} {s : Set X} : s ∈ 𝓝 a β†’ a ∈ s := fun H => +theorem mem_of_mem_nhds : s ∈ 𝓝 x β†’ x ∈ s := fun H => let ⟨_t, ht, _, hs⟩ := mem_nhds_iff.1 H; ht hs #align mem_of_mem_nhds mem_of_mem_nhds -/-- If a predicate is true in a neighborhood of `a`, then it is true for `a`. -/ -theorem Filter.Eventually.self_of_nhds {p : X β†’ Prop} {a : X} (h : βˆ€αΆ  y in 𝓝 a, p y) : p a := +/-- If a predicate is true in a neighborhood of `x`, then it is true for `x`. -/ +theorem Filter.Eventually.self_of_nhds {p : X β†’ Prop} (h : βˆ€αΆ  y in 𝓝 x, p y) : p x := mem_of_mem_nhds h #align filter.eventually.self_of_nhds Filter.Eventually.self_of_nhds -theorem IsOpen.mem_nhds {a : X} {s : Set X} (hs : IsOpen s) (ha : a ∈ s) : s ∈ 𝓝 a := - mem_nhds_iff.2 ⟨s, Subset.refl _, hs, ha⟩ +theorem IsOpen.mem_nhds (hs : IsOpen s) (hx : x ∈ s) : s ∈ 𝓝 x := + mem_nhds_iff.2 ⟨s, Subset.refl _, hs, hx⟩ #align is_open.mem_nhds IsOpen.mem_nhds -protected theorem IsOpen.mem_nhds_iff {a : X} {s : Set X} (hs : IsOpen s) : s ∈ 𝓝 a ↔ a ∈ s := - ⟨mem_of_mem_nhds, fun ha => mem_nhds_iff.2 ⟨s, Subset.rfl, hs, ha⟩⟩ +protected theorem IsOpen.mem_nhds_iff (hs : IsOpen s) : s ∈ 𝓝 x ↔ x ∈ s := + ⟨mem_of_mem_nhds, fun hx => mem_nhds_iff.2 ⟨s, Subset.rfl, hs, hx⟩⟩ #align is_open.mem_nhds_iff IsOpen.mem_nhds_iff -theorem IsClosed.compl_mem_nhds {a : X} {s : Set X} (hs : IsClosed s) (ha : a βˆ‰ s) : sᢜ ∈ 𝓝 a := - hs.isOpen_compl.mem_nhds (mem_compl ha) +theorem IsClosed.compl_mem_nhds (hs : IsClosed s) (hx : x βˆ‰ s) : sᢜ ∈ 𝓝 x := + hs.isOpen_compl.mem_nhds (mem_compl hx) #align is_closed.compl_mem_nhds IsClosed.compl_mem_nhds -theorem IsOpen.eventually_mem {a : X} {s : Set X} (hs : IsOpen s) (ha : a ∈ s) : - βˆ€αΆ  x in 𝓝 a, x ∈ s := - IsOpen.mem_nhds hs ha +theorem IsOpen.eventually_mem (hs : IsOpen s) (hx : x ∈ s) : + βˆ€αΆ  x in 𝓝 x, x ∈ s := + IsOpen.mem_nhds hs hx #align is_open.eventually_mem IsOpen.eventually_mem -/-- The open neighborhoods of `a` are a basis for the neighborhood filter. See `nhds_basis_opens` -for a variant using open sets around `a` instead. -/ -theorem nhds_basis_opens' (a : X) : - (𝓝 a).HasBasis (fun s : Set X => s ∈ 𝓝 a ∧ IsOpen s) fun x => x := by - convert nhds_basis_opens a using 2 +/-- The open neighborhoods of `x` are a basis for the neighborhood filter. See `nhds_basis_opens` +for a variant using open sets around `x` instead. -/ +theorem nhds_basis_opens' (x : X) : + (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsOpen s) fun x => x := by + convert nhds_basis_opens x using 2 exact and_congr_left_iff.2 IsOpen.mem_nhds_iff #align nhds_basis_opens' nhds_basis_opens' /-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of `s`: it contains an open set containing `s`. -/ -theorem exists_open_set_nhds {s U : Set X} (h : βˆ€ x ∈ s, U ∈ 𝓝 x) : +theorem exists_open_set_nhds {U : Set X} (h : βˆ€ x ∈ s, U ∈ 𝓝 x) : βˆƒ V : Set X, s βŠ† V ∧ IsOpen V ∧ V βŠ† U := ⟨interior U, fun x hx => mem_interior_iff_mem_nhds.2 <| h x hx, isOpen_interior, interior_subset⟩ #align exists_open_set_nhds exists_open_set_nhds /-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of s: it contains an open set containing `s`. -/ -theorem exists_open_set_nhds' {s U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) : +theorem exists_open_set_nhds' {U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) : βˆƒ V : Set X, s βŠ† V ∧ IsOpen V ∧ V βŠ† U := exists_open_set_nhds (by simpa using h) #align exists_open_set_nhds' exists_open_set_nhds' -/-- If a predicate is true in a neighbourhood of `a`, then for `y` sufficiently close -to `a` this predicate is true in a neighbourhood of `y`. -/ -theorem Filter.Eventually.eventually_nhds {p : X β†’ Prop} {a : X} (h : βˆ€αΆ  y in 𝓝 a, p y) : - βˆ€αΆ  y in 𝓝 a, βˆ€αΆ  x in 𝓝 y, p x := +/-- If a predicate is true in a neighbourhood of `x`, then for `y` sufficiently close +to `x` this predicate is true in a neighbourhood of `y`. -/ +theorem Filter.Eventually.eventually_nhds {p : X β†’ Prop} (h : βˆ€αΆ  y in 𝓝 x, p y) : + βˆ€αΆ  y in 𝓝 x, βˆ€αΆ  x in 𝓝 y, p x := let ⟨t, htp, hto, ha⟩ := eventually_nhds_iff.1 h eventually_nhds_iff.2 ⟨t, fun _x hx => eventually_nhds_iff.2 ⟨t, htp, hto, hx⟩, hto, ha⟩ #align filter.eventually.eventually_nhds Filter.Eventually.eventually_nhds @[simp] -theorem eventually_eventually_nhds {p : X β†’ Prop} {a : X} : - (βˆ€αΆ  y in 𝓝 a, βˆ€αΆ  x in 𝓝 y, p x) ↔ βˆ€αΆ  x in 𝓝 a, p x := +theorem eventually_eventually_nhds {p : X β†’ Prop} : + (βˆ€αΆ  y in 𝓝 x, βˆ€αΆ  x in 𝓝 y, p x) ↔ βˆ€αΆ  x in 𝓝 x, p x := ⟨fun h => h.self_of_nhds, fun h => h.eventually_nhds⟩ #align eventually_eventually_nhds eventually_eventually_nhds @[simp] -theorem frequently_frequently_nhds {p : X β†’ Prop} {a : X} : - (βˆƒαΆ  y in 𝓝 a, βˆƒαΆ  x in 𝓝 y, p x) ↔ βˆƒαΆ  x in 𝓝 a, p x := by +theorem frequently_frequently_nhds {p : X β†’ Prop} : + (βˆƒαΆ  x' in 𝓝 x, βˆƒαΆ  x'' in 𝓝 x', p x'') ↔ βˆƒαΆ  x in 𝓝 x, p x := by rw [← not_iff_not] simp only [not_frequently, eventually_eventually_nhds] #align frequently_frequently_nhds frequently_frequently_nhds @[simp] -theorem eventually_mem_nhds {s : Set X} {a : X} : (βˆ€αΆ  x in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a := +theorem eventually_mem_nhds : (βˆ€αΆ  x' in 𝓝 x, s ∈ 𝓝 x') ↔ s ∈ 𝓝 x := eventually_eventually_nhds #align eventually_mem_nhds eventually_mem_nhds @[simp] -theorem nhds_bind_nhds : (𝓝 a).bind 𝓝 = 𝓝 a := +theorem nhds_bind_nhds : (𝓝 x).bind 𝓝 = 𝓝 x := Filter.ext fun _ => eventually_eventually_nhds #align nhds_bind_nhds nhds_bind_nhds @[simp] -theorem eventually_eventuallyEq_nhds {f g : X β†’ Ξ±} {a : X} : - (βˆ€αΆ  y in 𝓝 a, f =αΆ [𝓝 y] g) ↔ f =αΆ [𝓝 a] g := +theorem eventually_eventuallyEq_nhds {f g : X β†’ Ξ±} : + (βˆ€αΆ  y in 𝓝 x, f =αΆ [𝓝 y] g) ↔ f =αΆ [𝓝 x] g := eventually_eventually_nhds #align eventually_eventually_eq_nhds eventually_eventuallyEq_nhds -theorem Filter.EventuallyEq.eq_of_nhds {f g : X β†’ Ξ±} {a : X} (h : f =αΆ [𝓝 a] g) : f a = g a := +theorem Filter.EventuallyEq.eq_of_nhds {f g : X β†’ Ξ±} (h : f =αΆ [𝓝 x] g) : f x = g x := h.self_of_nhds #align filter.eventually_eq.eq_of_nhds Filter.EventuallyEq.eq_of_nhds @[simp] -theorem eventually_eventuallyLE_nhds [LE Ξ±] {f g : X β†’ Ξ±} {a : X} : - (βˆ€αΆ  y in 𝓝 a, f ≀ᢠ[𝓝 y] g) ↔ f ≀ᢠ[𝓝 a] g := +theorem eventually_eventuallyLE_nhds [LE Ξ±] {f g : X β†’ Ξ±} : + (βˆ€αΆ  y in 𝓝 x, f ≀ᢠ[𝓝 y] g) ↔ f ≀ᢠ[𝓝 x] g := eventually_eventually_nhds #align eventually_eventually_le_nhds eventually_eventuallyLE_nhds -/-- If two functions are equal in a neighbourhood of `a`, then for `y` sufficiently close -to `a` these functions are equal in a neighbourhood of `y`. -/ -theorem Filter.EventuallyEq.eventuallyEq_nhds {f g : X β†’ Ξ±} {a : X} (h : f =αΆ [𝓝 a] g) : - βˆ€αΆ  y in 𝓝 a, f =αΆ [𝓝 y] g := +/-- If two functions are equal in a neighbourhood of `x`, then for `y` sufficiently close +to `x` these functions are equal in a neighbourhood of `y`. -/ +theorem Filter.EventuallyEq.eventuallyEq_nhds {f g : X β†’ Ξ±} (h : f =αΆ [𝓝 x] g) : + βˆ€αΆ  y in 𝓝 x, f =αΆ [𝓝 y] g := h.eventually_nhds #align filter.eventually_eq.eventually_eq_nhds Filter.EventuallyEq.eventuallyEq_nhds -/-- If `f x ≀ g x` in a neighbourhood of `a`, then for `y` sufficiently close to `a` we have +/-- If `f x ≀ g x` in a neighbourhood of `x`, then for `y` sufficiently close to `x` we have `f x ≀ g x` in a neighbourhood of `y`. -/ -theorem Filter.EventuallyLE.eventuallyLE_nhds [LE Ξ±] {f g : X β†’ Ξ±} {a : X} (h : f ≀ᢠ[𝓝 a] g) : - βˆ€αΆ  y in 𝓝 a, f ≀ᢠ[𝓝 y] g := +theorem Filter.EventuallyLE.eventuallyLE_nhds [LE Ξ±] {f g : X β†’ Ξ±} (h : f ≀ᢠ[𝓝 x] g) : + βˆ€αΆ  y in 𝓝 x, f ≀ᢠ[𝓝 y] g := h.eventually_nhds #align filter.eventually_le.eventually_le_nhds Filter.EventuallyLE.eventuallyLE_nhds @@ -1053,27 +1053,27 @@ theorem all_mem_nhds_filter (x : X) (f : Set X β†’ Set Ξ±) (hf : βˆ€ s t, s βŠ† all_mem_nhds _ _ fun s t ssubt h => mem_of_superset h (hf s t ssubt) #align all_mem_nhds_filter all_mem_nhds_filter -theorem tendsto_nhds {f : Ξ± β†’ X} {l : Filter Ξ±} {a : X} : - Tendsto f l (𝓝 a) ↔ βˆ€ s, IsOpen s β†’ a ∈ s β†’ f ⁻¹' s ∈ l := +theorem tendsto_nhds {f : Ξ± β†’ X} {l : Filter Ξ±} : + Tendsto f l (𝓝 x) ↔ βˆ€ s, IsOpen s β†’ x ∈ s β†’ f ⁻¹' s ∈ l := all_mem_nhds_filter _ _ (fun _ _ h => preimage_mono h) _ #align tendsto_nhds tendsto_nhds -theorem tendsto_atTop_nhds [Nonempty Ξ±] [SemilatticeSup Ξ±] {f : Ξ± β†’ X} {a : X} : - Tendsto f atTop (𝓝 a) ↔ βˆ€ U : Set X, a ∈ U β†’ IsOpen U β†’ βˆƒ N, βˆ€ n, N ≀ n β†’ f n ∈ U := - (atTop_basis.tendsto_iff (nhds_basis_opens a)).trans <| by +theorem tendsto_atTop_nhds [Nonempty Ξ±] [SemilatticeSup Ξ±] {f : Ξ± β†’ X} : + Tendsto f atTop (𝓝 x) ↔ βˆ€ U : Set X, x ∈ U β†’ IsOpen U β†’ βˆƒ N, βˆ€ n, N ≀ n β†’ f n ∈ U := + (atTop_basis.tendsto_iff (nhds_basis_opens x)).trans <| by simp only [and_imp, exists_prop, true_and_iff, mem_Ici, ge_iff_le] #align tendsto_at_top_nhds tendsto_atTop_nhds -theorem tendsto_const_nhds {a : X} {f : Filter Ξ±} : Tendsto (fun _ : Ξ± => a) f (𝓝 a) := +theorem tendsto_const_nhds {f : Filter Ξ±} : Tendsto (fun _ : Ξ± => x) f (𝓝 x) := tendsto_nhds.mpr fun _ _ ha => univ_mem' fun _ => ha #align tendsto_const_nhds tendsto_const_nhds -theorem tendsto_atTop_of_eventually_const {ΞΉ : Type*} [SemilatticeSup ΞΉ] [Nonempty ΞΉ] {x : X} +theorem tendsto_atTop_of_eventually_const {ΞΉ : Type*} [SemilatticeSup ΞΉ] [Nonempty ΞΉ] {u : ΞΉ β†’ X} {iβ‚€ : ΞΉ} (h : βˆ€ i β‰₯ iβ‚€, u i = x) : Tendsto u atTop (𝓝 x) := Tendsto.congr' (EventuallyEq.symm (eventually_atTop.mpr ⟨iβ‚€, h⟩)) tendsto_const_nhds #align tendsto_at_top_of_eventually_const tendsto_atTop_of_eventually_const -theorem tendsto_atBot_of_eventually_const {ΞΉ : Type*} [SemilatticeInf ΞΉ] [Nonempty ΞΉ] {x : X} +theorem tendsto_atBot_of_eventually_const {ΞΉ : Type*} [SemilatticeInf ΞΉ] [Nonempty ΞΉ] {u : ΞΉ β†’ X} {iβ‚€ : ΞΉ} (h : βˆ€ i ≀ iβ‚€, u i = x) : Tendsto u atBot (𝓝 x) := Tendsto.congr' (EventuallyEq.symm (eventually_atBot.mpr ⟨iβ‚€, h⟩)) tendsto_const_nhds #align tendsto_at_bot_of_eventually_const tendsto_atBot_of_eventually_const @@ -1091,16 +1091,16 @@ theorem OrderTop.tendsto_atTop_nhds [PartialOrder Ξ±] [OrderTop Ξ±] (f : Ξ± β†’ #align order_top.tendsto_at_top_nhds OrderTop.tendsto_atTop_nhds @[simp] -instance nhds_neBot {a : X} : NeBot (𝓝 a) := - neBot_of_le (pure_le_nhds a) +instance nhds_neBot : NeBot (𝓝 x) := + neBot_of_le (pure_le_nhds x) #align nhds_ne_bot nhds_neBot -theorem tendsto_nhds_of_eventually_eq {l : Filter Ξ±} {f : Ξ± β†’ X} {a : X} (h : βˆ€αΆ  x in l, f x = a) : - Tendsto f l (𝓝 a) := +theorem tendsto_nhds_of_eventually_eq {l : Filter Ξ±} {f : Ξ± β†’ X} (h : βˆ€αΆ  x' in l, f x' = x) : + Tendsto f l (𝓝 x) := tendsto_const_nhds.congr' (.symm h) -theorem Filter.EventuallyEq.tendsto {l : Filter Ξ±} {f : Ξ± β†’ X} {a : X} (hf : f =αΆ [l] fun _ ↦ a) : - Tendsto f l (𝓝 a) := +theorem Filter.EventuallyEq.tendsto {l : Filter Ξ±} {f : Ξ± β†’ X} (hf : f =αΆ [l] fun _ ↦ x) : + Tendsto f l (𝓝 x) := tendsto_nhds_of_eventually_eq hf /-! @@ -1118,64 +1118,64 @@ def ClusterPt (x : X) (F : Filter X) : Prop := NeBot (𝓝 x βŠ“ F) #align cluster_pt ClusterPt -theorem ClusterPt.neBot {x : X} {F : Filter X} (h : ClusterPt x F) : NeBot (𝓝 x βŠ“ F) := +theorem ClusterPt.neBot {F : Filter X} (h : ClusterPt x F) : NeBot (𝓝 x βŠ“ F) := h #align cluster_pt.ne_bot ClusterPt.neBot -theorem Filter.HasBasis.clusterPt_iff {ΞΉa ΞΉF} {pa : ΞΉa β†’ Prop} {sa : ΞΉa β†’ Set X} {pF : ΞΉF β†’ Prop} - {sF : ΞΉF β†’ Set X} {F : Filter X} (ha : (𝓝 a).HasBasis pa sa) (hF : F.HasBasis pF sF) : - ClusterPt a F ↔ βˆ€ ⦃i⦄, pa i β†’ βˆ€ ⦃j⦄, pF j β†’ (sa i ∩ sF j).Nonempty := - ha.inf_basis_neBot_iff hF +theorem Filter.HasBasis.clusterPt_iff {ΞΉX ΞΉF} {pX : ΞΉX β†’ Prop} {sX : ΞΉX β†’ Set X} {pF : ΞΉF β†’ Prop} + {sF : ΞΉF β†’ Set X} {F : Filter X} (hX : (𝓝 x).HasBasis pX sX) (hF : F.HasBasis pF sF) : + ClusterPt x F ↔ βˆ€ ⦃i⦄, pX i β†’ βˆ€ ⦃j⦄, pF j β†’ (sX i ∩ sF j).Nonempty := + hX.inf_basis_neBot_iff hF #align filter.has_basis.cluster_pt_iff Filter.HasBasis.clusterPt_iff -theorem clusterPt_iff {x : X} {F : Filter X} : +theorem clusterPt_iff {F : Filter X} : ClusterPt x F ↔ βˆ€ ⦃U : Set X⦄, U ∈ 𝓝 x β†’ βˆ€ ⦃V⦄, V ∈ F β†’ (U ∩ V).Nonempty := inf_neBot_iff #align cluster_pt_iff clusterPt_iff -theorem clusterPt_iff_not_disjoint {x : X} {F : Filter X} : +theorem clusterPt_iff_not_disjoint {F : Filter X} : ClusterPt x F ↔ Β¬Disjoint (𝓝 x) F := by rw [disjoint_iff, ClusterPt, neBot_iff] /-- `x` is a cluster point of a set `s` if every neighbourhood of `x` meets `s` on a nonempty set. See also `mem_closure_iff_clusterPt`. -/ -theorem clusterPt_principal_iff {x : X} {s : Set X} : +theorem clusterPt_principal_iff : ClusterPt x (π“Ÿ s) ↔ βˆ€ U ∈ 𝓝 x, (U ∩ s).Nonempty := inf_principal_neBot_iff #align cluster_pt_principal_iff clusterPt_principal_iff -theorem clusterPt_principal_iff_frequently {x : X} {s : Set X} : +theorem clusterPt_principal_iff_frequently : ClusterPt x (π“Ÿ s) ↔ βˆƒαΆ  y in 𝓝 x, y ∈ s := by simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, exists_prop, mem_inter_iff] #align cluster_pt_principal_iff_frequently clusterPt_principal_iff_frequently -theorem ClusterPt.of_le_nhds {x : X} {f : Filter X} (H : f ≀ 𝓝 x) [NeBot f] : ClusterPt x f := by +theorem ClusterPt.of_le_nhds {f : Filter X} (H : f ≀ 𝓝 x) [NeBot f] : ClusterPt x f := by rwa [ClusterPt, inf_eq_right.mpr H] #align cluster_pt.of_le_nhds ClusterPt.of_le_nhds -theorem ClusterPt.of_le_nhds' {x : X} {f : Filter X} (H : f ≀ 𝓝 x) (_hf : NeBot f) : +theorem ClusterPt.of_le_nhds' {f : Filter X} (H : f ≀ 𝓝 x) (_hf : NeBot f) : ClusterPt x f := ClusterPt.of_le_nhds H #align cluster_pt.of_le_nhds' ClusterPt.of_le_nhds' -theorem ClusterPt.of_nhds_le {x : X} {f : Filter X} (H : 𝓝 x ≀ f) : ClusterPt x f := by +theorem ClusterPt.of_nhds_le {f : Filter X} (H : 𝓝 x ≀ f) : ClusterPt x f := by simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot] #align cluster_pt.of_nhds_le ClusterPt.of_nhds_le -theorem ClusterPt.mono {x : X} {f g : Filter X} (H : ClusterPt x f) (h : f ≀ g) : ClusterPt x g := +theorem ClusterPt.mono {f g : Filter X} (H : ClusterPt x f) (h : f ≀ g) : ClusterPt x g := NeBot.mono H <| inf_le_inf_left _ h #align cluster_pt.mono ClusterPt.mono -theorem ClusterPt.of_inf_left {x : X} {f g : Filter X} (H : ClusterPt x <| f βŠ“ g) : ClusterPt x f := +theorem ClusterPt.of_inf_left {f g : Filter X} (H : ClusterPt x <| f βŠ“ g) : ClusterPt x f := H.mono inf_le_left #align cluster_pt.of_inf_left ClusterPt.of_inf_left -theorem ClusterPt.of_inf_right {x : X} {f g : Filter X} (H : ClusterPt x <| f βŠ“ g) : +theorem ClusterPt.of_inf_right {f g : Filter X} (H : ClusterPt x <| f βŠ“ g) : ClusterPt x g := H.mono inf_le_right #align cluster_pt.of_inf_right ClusterPt.of_inf_right -theorem Ultrafilter.clusterPt_iff {x : X} {f : Ultrafilter X} : ClusterPt x f ↔ ↑f ≀ 𝓝 x := +theorem Ultrafilter.clusterPt_iff {f : Ultrafilter X} : ClusterPt x f ↔ ↑f ≀ 𝓝 x := ⟨f.le_of_inf_neBot', fun h => ClusterPt.of_le_nhds h⟩ #align ultrafilter.cluster_pt_iff Ultrafilter.clusterPt_iff @@ -1191,7 +1191,7 @@ theorem mapClusterPt_iff {ΞΉ : Type*} (x : X) (F : Filter ΞΉ) (u : ΞΉ β†’ X) : rfl #align map_cluster_pt_iff mapClusterPt_iff -theorem mapClusterPt_of_comp {F : Filter Ξ±} {Ο† : Ξ² β†’ Ξ±} {p : Filter Ξ²} {x : X} +theorem mapClusterPt_of_comp {F : Filter Ξ±} {Ο† : Ξ² β†’ Ξ±} {p : Filter Ξ²} {u : Ξ± β†’ X} [NeBot p] (h : Tendsto Ο† p F) (H : Tendsto (u ∘ Ο†) p (𝓝 x)) : MapClusterPt x F u := by have := @@ -1232,7 +1232,7 @@ theorem accPt_iff_frequently (x : X) (C : Set X) : AccPt x (π“Ÿ C) ↔ βˆƒαΆ  y /-- If `x` is an accumulation point of `F` and `F ≀ G`, then `x` is an accumulation point of `D`. -/ -theorem AccPt.mono {x : X} {F G : Filter X} (h : AccPt x F) (hFG : F ≀ G) : AccPt x G := +theorem AccPt.mono {F G : Filter X} (h : AccPt x F) (hFG : F ≀ G) : AccPt x G := NeBot.mono h (inf_le_inf_left _ hFG) #align acc_pt.mono AccPt.mono @@ -1240,16 +1240,16 @@ theorem AccPt.mono {x : X} {F G : Filter X} (h : AccPt x F) (hFG : F ≀ G) : Ac ### Interior, closure and frontier in terms of neighborhoods -/ -theorem interior_eq_nhds' {s : Set X} : interior s = { a | s ∈ 𝓝 a } := +theorem interior_eq_nhds' : interior s = { x | s ∈ 𝓝 x } := Set.ext fun x => by simp only [mem_interior, mem_nhds_iff, mem_setOf_eq] #align interior_eq_nhds' interior_eq_nhds' -theorem interior_eq_nhds {s : Set X} : interior s = { a | 𝓝 a ≀ π“Ÿ s } := +theorem interior_eq_nhds : interior s = { x | 𝓝 x ≀ π“Ÿ s } := interior_eq_nhds'.trans <| by simp only [le_principal_iff] #align interior_eq_nhds interior_eq_nhds @[simp] -theorem interior_mem_nhds {s : Set X} {a : X} : interior s ∈ 𝓝 a ↔ s ∈ 𝓝 a := +theorem interior_mem_nhds : interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x := ⟨fun h => mem_of_superset h interior_subset, fun h => IsOpen.mem_nhds isOpen_interior (mem_interior_iff_mem_nhds.2 h)⟩ #align interior_mem_nhds interior_mem_nhds @@ -1262,46 +1262,46 @@ theorem isOpen_setOf_eventually_nhds {p : X β†’ Prop} : IsOpen { x | βˆ€αΆ  y in simp only [← interior_setOf_eq, isOpen_interior] #align is_open_set_of_eventually_nhds isOpen_setOf_eventually_nhds -theorem subset_interior_iff_nhds {s V : Set X} : s βŠ† interior V ↔ βˆ€ x ∈ s, V ∈ 𝓝 x := by +theorem subset_interior_iff_nhds {V : Set X} : s βŠ† interior V ↔ βˆ€ x ∈ s, V ∈ 𝓝 x := by simp_rw [subset_def, mem_interior_iff_mem_nhds] #align subset_interior_iff_nhds subset_interior_iff_nhds -theorem isOpen_iff_nhds {s : Set X} : IsOpen s ↔ βˆ€ a ∈ s, 𝓝 a ≀ π“Ÿ s := +theorem isOpen_iff_nhds : IsOpen s ↔ βˆ€ x ∈ s, 𝓝 x ≀ π“Ÿ s := calc IsOpen s ↔ s βŠ† interior s := subset_interior_iff_isOpen.symm - _ ↔ βˆ€ a ∈ s, 𝓝 a ≀ π“Ÿ s := by simp_rw [interior_eq_nhds, subset_def, mem_setOf] + _ ↔ βˆ€ x ∈ s, 𝓝 x ≀ π“Ÿ s := by simp_rw [interior_eq_nhds, subset_def, mem_setOf] #align is_open_iff_nhds isOpen_iff_nhds -theorem isOpen_iff_mem_nhds {s : Set X} : IsOpen s ↔ βˆ€ a ∈ s, s ∈ 𝓝 a := +theorem isOpen_iff_mem_nhds : IsOpen s ↔ βˆ€ x ∈ s, s ∈ 𝓝 x := isOpen_iff_nhds.trans <| forall_congr' fun _ => imp_congr_right fun _ => le_principal_iff #align is_open_iff_mem_nhds isOpen_iff_mem_nhds /-- A set `s` is open iff for every point `x` in `s` and every `y` close to `x`, `y` is in `s`. -/ -theorem isOpen_iff_eventually {s : Set X} : IsOpen s ↔ βˆ€ x, x ∈ s β†’ βˆ€αΆ  y in 𝓝 x, y ∈ s := +theorem isOpen_iff_eventually : IsOpen s ↔ βˆ€ x, x ∈ s β†’ βˆ€αΆ  y in 𝓝 x, y ∈ s := isOpen_iff_mem_nhds #align is_open_iff_eventually isOpen_iff_eventually -theorem isOpen_iff_ultrafilter {s : Set X} : +theorem isOpen_iff_ultrafilter : IsOpen s ↔ βˆ€ x ∈ s, βˆ€ (l : Ultrafilter X), ↑l ≀ 𝓝 x β†’ s ∈ l := by simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter] #align is_open_iff_ultrafilter isOpen_iff_ultrafilter -theorem isOpen_singleton_iff_nhds_eq_pure (a : X) : IsOpen ({a} : Set X) ↔ 𝓝 a = pure a := by +theorem isOpen_singleton_iff_nhds_eq_pure (x : X) : IsOpen ({x} : Set X) ↔ 𝓝 x = pure x := by constructor Β· intro h - apply le_antisymm _ (pure_le_nhds a) + apply le_antisymm _ (pure_le_nhds x) rw [le_pure_iff] - exact h.mem_nhds (mem_singleton a) + exact h.mem_nhds (mem_singleton x) Β· intro h simp [isOpen_iff_nhds, h] #align is_open_singleton_iff_nhds_eq_pure isOpen_singleton_iff_nhds_eq_pure -theorem isOpen_singleton_iff_punctured_nhds (a : X) : IsOpen ({a} : Set X) ↔ 𝓝[β‰ ] a = βŠ₯ := by +theorem isOpen_singleton_iff_punctured_nhds (x : X) : IsOpen ({x} : Set X) ↔ 𝓝[β‰ ] x = βŠ₯ := by rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl, ← le_pure_iff, nhds_neBot.le_pure_iff] #align is_open_singleton_iff_punctured_nhds isOpen_singleton_iff_punctured_nhds -theorem mem_closure_iff_frequently {s : Set X} {a : X} : a ∈ closure s ↔ βˆƒαΆ  x in 𝓝 a, x ∈ s := by +theorem mem_closure_iff_frequently : x ∈ closure s ↔ βˆƒαΆ  x in 𝓝 x, x ∈ s := by rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds, closure_eq_compl_interior_compl, mem_compl_iff, compl_def] #align mem_closure_iff_frequently mem_closure_iff_frequently @@ -1311,7 +1311,7 @@ alias ⟨_, Filter.Frequently.mem_closure⟩ := mem_closure_iff_frequently /-- A set `s` is closed iff for every point `x`, if there is a point `y` close to `x` that belongs to `s` then `x` is in `s`. -/ -theorem isClosed_iff_frequently {s : Set X} : IsClosed s ↔ βˆ€ x, (βˆƒαΆ  y in 𝓝 x, y ∈ s) β†’ x ∈ s := by +theorem isClosed_iff_frequently : IsClosed s ↔ βˆ€ x, (βˆƒαΆ  y in 𝓝 x, y ∈ s) β†’ x ∈ s := by rw [← closure_subset_iff_isClosed] refine' forall_congr' fun x => _ rw [mem_closure_iff_frequently] @@ -1325,19 +1325,19 @@ theorem isClosed_setOf_clusterPt {f : Filter X} : IsClosed { x | ClusterPt x f } exacts [isOpen_setOf_eventually_nhds, isOpen_const] #align is_closed_set_of_cluster_pt isClosed_setOf_clusterPt -theorem mem_closure_iff_clusterPt {s : Set X} {a : X} : a ∈ closure s ↔ ClusterPt a (π“Ÿ s) := +theorem mem_closure_iff_clusterPt : x ∈ closure s ↔ ClusterPt x (π“Ÿ s) := mem_closure_iff_frequently.trans clusterPt_principal_iff_frequently.symm #align mem_closure_iff_cluster_pt mem_closure_iff_clusterPt -theorem mem_closure_iff_nhds_neBot {s : Set X} : a ∈ closure s ↔ 𝓝 a βŠ“ π“Ÿ s β‰  βŠ₯ := +theorem mem_closure_iff_nhds_neBot : x ∈ closure s ↔ 𝓝 x βŠ“ π“Ÿ s β‰  βŠ₯ := mem_closure_iff_clusterPt.trans neBot_iff #align mem_closure_iff_nhds_ne_bot mem_closure_iff_nhds_neBot -theorem mem_closure_iff_nhdsWithin_neBot {s : Set X} {x : X} : x ∈ closure s ↔ NeBot (𝓝[s] x) := +theorem mem_closure_iff_nhdsWithin_neBot : x ∈ closure s ↔ NeBot (𝓝[s] x) := mem_closure_iff_clusterPt #align mem_closure_iff_nhds_within_ne_bot mem_closure_iff_nhdsWithin_neBot -lemma not_mem_closure_iff_nhdsWithin_eq_bot {s : Set X} {x : X} : x βˆ‰ closure s ↔ 𝓝[s] x = βŠ₯ := by +lemma not_mem_closure_iff_nhdsWithin_eq_bot : x βˆ‰ closure s ↔ 𝓝[s] x = βŠ₯ := by rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] /-- If `x` is not an isolated point of a topological space, then `{x}ᢜ` is dense in the whole @@ -1366,81 +1366,81 @@ theorem not_isOpen_singleton (x : X) [NeBot (𝓝[β‰ ] x)] : Β¬IsOpen ({x} : Set dense_compl_singleton_iff_not_open.1 (dense_compl_singleton x) #align not_is_open_singleton not_isOpen_singleton -theorem closure_eq_cluster_pts {s : Set X} : closure s = { a | ClusterPt a (π“Ÿ s) } := +theorem closure_eq_cluster_pts : closure s = { a | ClusterPt a (π“Ÿ s) } := Set.ext fun _ => mem_closure_iff_clusterPt #align closure_eq_cluster_pts closure_eq_cluster_pts -theorem mem_closure_iff_nhds {s : Set X} {a : X} : a ∈ closure s ↔ βˆ€ t ∈ 𝓝 a, (t ∩ s).Nonempty := +theorem mem_closure_iff_nhds : x ∈ closure s ↔ βˆ€ t ∈ 𝓝 x, (t ∩ s).Nonempty := mem_closure_iff_clusterPt.trans clusterPt_principal_iff #align mem_closure_iff_nhds mem_closure_iff_nhds -theorem mem_closure_iff_nhds' {s : Set X} {a : X} : a ∈ closure s ↔ βˆ€ t ∈ 𝓝 a, βˆƒ y : s, ↑y ∈ t := by +theorem mem_closure_iff_nhds' : x ∈ closure s ↔ βˆ€ t ∈ 𝓝 x, βˆƒ y : s, ↑y ∈ t := by simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop] #align mem_closure_iff_nhds' mem_closure_iff_nhds' -theorem mem_closure_iff_comap_neBot {A : Set X} {x : X} : - x ∈ closure A ↔ NeBot (comap ((↑) : A β†’ X) (𝓝 x)) := by +theorem mem_closure_iff_comap_neBot : + x ∈ closure s ↔ NeBot (comap ((↑) : s β†’ X) (𝓝 x)) := by simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop] #align mem_closure_iff_comap_ne_bot mem_closure_iff_comap_neBot -theorem mem_closure_iff_nhds_basis' {a : X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : (𝓝 a).HasBasis p s) - {t : Set X} : a ∈ closure t ↔ βˆ€ i, p i β†’ (s i ∩ t).Nonempty := +theorem mem_closure_iff_nhds_basis' {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : (𝓝 x).HasBasis p s) : + x ∈ closure t ↔ βˆ€ i, p i β†’ (s i ∩ t).Nonempty := mem_closure_iff_clusterPt.trans <| (h.clusterPt_iff (hasBasis_principal _)).trans <| by simp only [exists_prop, forall_const] #align mem_closure_iff_nhds_basis' mem_closure_iff_nhds_basis' -theorem mem_closure_iff_nhds_basis {a : X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : (𝓝 a).HasBasis p s) - {t : Set X} : a ∈ closure t ↔ βˆ€ i, p i β†’ βˆƒ y ∈ t, y ∈ s i := +theorem mem_closure_iff_nhds_basis {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : (𝓝 x).HasBasis p s) : + x ∈ closure t ↔ βˆ€ i, p i β†’ βˆƒ y ∈ t, y ∈ s i := (mem_closure_iff_nhds_basis' h).trans <| by simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm] #align mem_closure_iff_nhds_basis mem_closure_iff_nhds_basis -theorem clusterPt_iff_forall_mem_closure {F : Filter X} {a : X} : - ClusterPt a F ↔ βˆ€ s ∈ F, a ∈ closure s := by +theorem clusterPt_iff_forall_mem_closure {F : Filter X} : + ClusterPt x F ↔ βˆ€ s ∈ F, x ∈ closure s := by simp_rw [ClusterPt, inf_neBot_iff, mem_closure_iff_nhds] rw [forallβ‚‚_swap] -theorem clusterPt_iff_lift'_closure {F : Filter X} {a : X} : - ClusterPt a F ↔ pure a ≀ (F.lift' closure) := by +theorem clusterPt_iff_lift'_closure {F : Filter X} : + ClusterPt x F ↔ pure x ≀ (F.lift' closure) := by simp_rw [clusterPt_iff_forall_mem_closure, (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and, exists_const] -theorem clusterPt_iff_lift'_closure' {F : Filter X} {a : X} : - ClusterPt a F ↔ (F.lift' closure βŠ“ pure a).NeBot := by +theorem clusterPt_iff_lift'_closure' {F : Filter X} : + ClusterPt x F ↔ (F.lift' closure βŠ“ pure x).NeBot := by rw [clusterPt_iff_lift'_closure, ← Ultrafilter.coe_pure, inf_comm, Ultrafilter.inf_neBot_iff] @[simp] -theorem clusterPt_lift'_closure_iff {F : Filter X} {a : X} : - ClusterPt a (F.lift' closure) ↔ ClusterPt a F := by +theorem clusterPt_lift'_closure_iff {F : Filter X} : + ClusterPt x (F.lift' closure) ↔ ClusterPt x F := by simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)] /-- `x` belongs to the closure of `s` if and only if some ultrafilter supported on `s` converges to `x`. -/ -theorem mem_closure_iff_ultrafilter {s : Set X} {x : X} : +theorem mem_closure_iff_ultrafilter : x ∈ closure s ↔ βˆƒ u : Ultrafilter X, s ∈ u ∧ ↑u ≀ 𝓝 x := by simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm] #align mem_closure_iff_ultrafilter mem_closure_iff_ultrafilter -theorem isClosed_iff_clusterPt {s : Set X} : IsClosed s ↔ βˆ€ a, ClusterPt a (π“Ÿ s) β†’ a ∈ s := +theorem isClosed_iff_clusterPt : IsClosed s ↔ βˆ€ a, ClusterPt a (π“Ÿ s) β†’ a ∈ s := calc IsClosed s ↔ closure s βŠ† s := closure_subset_iff_isClosed.symm _ ↔ βˆ€ a, ClusterPt a (π“Ÿ s) β†’ a ∈ s := by simp only [subset_def, mem_closure_iff_clusterPt] #align is_closed_iff_cluster_pt isClosed_iff_clusterPt -theorem isClosed_iff_nhds {s : Set X} : +theorem isClosed_iff_nhds : IsClosed s ↔ βˆ€ x, (βˆ€ U ∈ 𝓝 x, (U ∩ s).Nonempty) β†’ x ∈ s := by simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff] #align is_closed_iff_nhds isClosed_iff_nhds -lemma isClosed_iff_forall_filter {s : Set X} : +lemma isClosed_iff_forall_filter : IsClosed s ↔ βˆ€ x, βˆ€ F : Filter X, F.NeBot β†’ F ≀ π“Ÿ s β†’ F ≀ 𝓝 x β†’ x ∈ s := by simp_rw [isClosed_iff_clusterPt] exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS), fun hs x hx ↦ hs x (𝓝 x βŠ“ π“Ÿ s) hx inf_le_right inf_le_left⟩ -theorem IsClosed.interior_union_left {s t : Set X} (_ : IsClosed s) : +theorem IsClosed.interior_union_left (_ : IsClosed s) : interior (s βˆͺ t) βŠ† s βˆͺ interior t := fun a ⟨u, ⟨⟨hu₁, huβ‚‚βŸ©, ha⟩⟩ => (Classical.em (a ∈ s)).imp_right fun h => mem_interior.mpr @@ -1448,28 +1448,28 @@ theorem IsClosed.interior_union_left {s t : Set X} (_ : IsClosed s) : ⟨ha, h⟩⟩ #align is_closed.interior_union_left IsClosed.interior_union_left -theorem IsClosed.interior_union_right {s t : Set X} (h : IsClosed t) : +theorem IsClosed.interior_union_right (h : IsClosed t) : interior (s βˆͺ t) βŠ† interior s βˆͺ t := by simpa only [union_comm _ t] using h.interior_union_left #align is_closed.interior_union_right IsClosed.interior_union_right -theorem IsOpen.inter_closure {s t : Set X} (h : IsOpen s) : s ∩ closure t βŠ† closure (s ∩ t) := +theorem IsOpen.inter_closure (h : IsOpen s) : s ∩ closure t βŠ† closure (s ∩ t) := compl_subset_compl.mp <| by simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl #align is_open.inter_closure IsOpen.inter_closure -theorem IsOpen.closure_inter {s t : Set X} (h : IsOpen t) : closure s ∩ t βŠ† closure (s ∩ t) := by +theorem IsOpen.closure_inter (h : IsOpen t) : closure s ∩ t βŠ† closure (s ∩ t) := by simpa only [inter_comm t] using h.inter_closure #align is_open.closure_inter IsOpen.closure_inter -theorem Dense.open_subset_closure_inter {s t : Set X} (hs : Dense s) (ht : IsOpen t) : +theorem Dense.open_subset_closure_inter (hs : Dense s) (ht : IsOpen t) : t βŠ† closure (t ∩ s) := calc t = t ∩ closure s := by rw [hs.closure_eq, inter_univ] _ βŠ† closure (t ∩ s) := ht.inter_closure #align dense.open_subset_closure_inter Dense.open_subset_closure_inter -theorem mem_closure_of_mem_closure_union {s₁ sβ‚‚ : Set X} {x : X} (h : x ∈ closure (s₁ βˆͺ sβ‚‚)) +theorem mem_closure_of_mem_closure_union (h : x ∈ closure (s₁ βˆͺ sβ‚‚)) (h₁ : sβ‚αΆœ ∈ 𝓝 x) : x ∈ closure sβ‚‚ := by rw [mem_closure_iff_nhds_neBot] at * rwa [← @@ -1482,24 +1482,24 @@ theorem mem_closure_of_mem_closure_union {s₁ sβ‚‚ : Set X} {x : X} (h : x ∈ #align mem_closure_of_mem_closure_union mem_closure_of_mem_closure_union /-- The intersection of an open dense set with a dense set is a dense set. -/ -theorem Dense.inter_of_isOpen_left {s t : Set X} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : +theorem Dense.inter_of_isOpen_left (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t) := fun x => closure_minimal hso.inter_closure isClosed_closure <| by simp [hs.closure_eq, ht.closure_eq] #align dense.inter_of_open_left Dense.inter_of_isOpen_left /-- The intersection of a dense set with an open dense set is a dense set. -/ -theorem Dense.inter_of_isOpen_right {s t : Set X} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : +theorem Dense.inter_of_isOpen_right (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t) := inter_comm t s β–Έ ht.inter_of_isOpen_left hs hto #align dense.inter_of_open_right Dense.inter_of_isOpen_right -theorem Dense.inter_nhds_nonempty {s t : Set X} (hs : Dense s) {x : X} (ht : t ∈ 𝓝 x) : +theorem Dense.inter_nhds_nonempty (hs : Dense s) (ht : t ∈ 𝓝 x) : (s ∩ t).Nonempty := let ⟨U, hsub, ho, hx⟩ := mem_nhds_iff.1 ht (hs.inter_open_nonempty U ho ⟨x, hx⟩).mono fun _y hy => ⟨hy.2, hsub hy.1⟩ #align dense.inter_nhds_nonempty Dense.inter_nhds_nonempty -theorem closure_diff {s t : Set X} : closure s \ closure t βŠ† closure (s \ t) := +theorem closure_diff : closure s \ closure t βŠ† closure (s \ t) := calc closure s \ closure t = (closure t)ᢜ ∩ closure s := by simp only [diff_eq, inter_comm] _ βŠ† closure ((closure t)ᢜ ∩ s) := (isOpen_compl_iff.mpr <| isClosed_closure).inter_closure @@ -1507,37 +1507,37 @@ theorem closure_diff {s t : Set X} : closure s \ closure t βŠ† closure (s \ t) : _ βŠ† closure (s \ t) := closure_mono <| diff_subset_diff (Subset.refl s) subset_closure #align closure_diff closure_diff -theorem Filter.Frequently.mem_of_closed {a : X} {s : Set X} (h : βˆƒαΆ  x in 𝓝 a, x ∈ s) - (hs : IsClosed s) : a ∈ s := +theorem Filter.Frequently.mem_of_closed (h : βˆƒαΆ  x in 𝓝 x, x ∈ s) + (hs : IsClosed s) : x ∈ s := hs.closure_subset h.mem_closure #align filter.frequently.mem_of_closed Filter.Frequently.mem_of_closed -theorem IsClosed.mem_of_frequently_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} {a : X} {s : Set X} - (hs : IsClosed s) (h : βˆƒαΆ  x in b, f x ∈ s) (hf : Tendsto f b (𝓝 a)) : a ∈ s := +theorem IsClosed.mem_of_frequently_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} + (hs : IsClosed s) (h : βˆƒαΆ  x in b, f x ∈ s) (hf : Tendsto f b (𝓝 x)) : x ∈ s := (hf.frequently <| show βˆƒαΆ  x in b, (fun y => y ∈ s) (f x) from h).mem_of_closed hs #align is_closed.mem_of_frequently_of_tendsto IsClosed.mem_of_frequently_of_tendsto -theorem IsClosed.mem_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} {a : X} {s : Set X} [NeBot b] - (hs : IsClosed s) (hf : Tendsto f b (𝓝 a)) (h : βˆ€αΆ  x in b, f x ∈ s) : a ∈ s := +theorem IsClosed.mem_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} [NeBot b] + (hs : IsClosed s) (hf : Tendsto f b (𝓝 x)) (h : βˆ€αΆ  x in b, f x ∈ s) : x ∈ s := hs.mem_of_frequently_of_tendsto h.frequently hf #align is_closed.mem_of_tendsto IsClosed.mem_of_tendsto -theorem mem_closure_of_frequently_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} {a : X} {s : Set X} - (h : βˆƒαΆ  x in b, f x ∈ s) (hf : Tendsto f b (𝓝 a)) : a ∈ closure s := +theorem mem_closure_of_frequently_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} + (h : βˆƒαΆ  x in b, f x ∈ s) (hf : Tendsto f b (𝓝 x)) : x ∈ closure s := (hf.frequently h).mem_closure #align mem_closure_of_frequently_of_tendsto mem_closure_of_frequently_of_tendsto -theorem mem_closure_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} {a : X} {s : Set X} [NeBot b] - (hf : Tendsto f b (𝓝 a)) (h : βˆ€αΆ  x in b, f x ∈ s) : a ∈ closure s := +theorem mem_closure_of_tendsto {f : Ξ± β†’ X} {b : Filter Ξ±} [NeBot b] + (hf : Tendsto f b (𝓝 x)) (h : βˆ€αΆ  x in b, f x ∈ s) : x ∈ closure s := mem_closure_of_frequently_of_tendsto h.frequently hf #align mem_closure_of_tendsto mem_closure_of_tendsto -/-- Suppose that `f` sends the complement to `s` to a single point `a`, and `l` is some filter. -Then `f` tends to `a` along `l` restricted to `s` if and only if it tends to `a` along `l`. -/ -theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : Ξ± β†’ X} {l : Filter Ξ±} {s : Set Ξ±} {a : X} - (h : βˆ€ x βˆ‰ s, f x = a) : Tendsto f (l βŠ“ π“Ÿ s) (𝓝 a) ↔ Tendsto f l (𝓝 a) := by +/-- Suppose that `f` sends the complement to `s` to a single point `x`, and `l` is some filter. +Then `f` tends to `x` along `l` restricted to `s` if and only if it tends to `x` along `l`. -/ +theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : Ξ± β†’ X} {l : Filter Ξ±} {s : Set Ξ±} + (h : βˆ€ a βˆ‰ s, f a = x) : Tendsto f (l βŠ“ π“Ÿ s) (𝓝 x) ↔ Tendsto f l (𝓝 x) := by rw [tendsto_iff_comap, tendsto_iff_comap] - replace h : π“Ÿ sᢜ ≀ comap f (𝓝 a) + replace h : π“Ÿ sᢜ ≀ comap f (𝓝 x) Β· rintro U ⟨t, ht, htU⟩ x hx have : f x ∈ t := (h x hx).symm β–Έ mem_of_mem_nhds ht exact htU this @@ -1554,7 +1554,7 @@ theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : Ξ± β†’ X} {l : Filter In this section we define functions that return a limit of a filter (or of a function along a filter), if it exists, and a random point otherwise. These functions are rarely used in Mathlib, most of the theorems are written using `Filter.Tendsto`. One of the reasons is that -`Filter.limUnder f g = a` is not equivalent to `Filter.Tendsto g f (𝓝 a)` unless the codomain is a +`Filter.limUnder f g = x` is not equivalent to `Filter.Tendsto g f (𝓝 x)` unless the codomain is a Hausdorff space and `g` has a limit along `f`. -/ @@ -1565,7 +1565,7 @@ set_option linter.uppercaseLean3 false /-- If `f` is a filter, then `Filter.lim f` is a limit of the filter, if it exists. -/ noncomputable def lim [Nonempty X] (f : Filter X) : X := - Classical.epsilon fun a => f ≀ 𝓝 a + Classical.epsilon fun x => f ≀ 𝓝 x #align Lim lim /-- @@ -1582,19 +1582,19 @@ noncomputable def limUnder [Nonempty X] (f : Filter Ξ±) (g : Ξ± β†’ X) : X := lim (f.map g) #align lim limUnder -/-- If a filter `f` is majorated by some `𝓝 a`, then it is majorated by `𝓝 (Filter.lim f)`. We +/-- If a filter `f` is majorated by some `𝓝 x`, then it is majorated by `𝓝 (Filter.lim f)`. We formulate this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for types without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance. -/ -theorem le_nhds_lim {f : Filter X} (h : βˆƒ a, f ≀ 𝓝 a) : f ≀ 𝓝 (@lim _ _ (nonempty_of_exists h) f) := +theorem le_nhds_lim {f : Filter X} (h : βˆƒ x, f ≀ 𝓝 x) : f ≀ 𝓝 (@lim _ _ (nonempty_of_exists h) f) := Classical.epsilon_spec h #align le_nhds_Lim le_nhds_lim -/-- If `g` tends to some `𝓝 a` along `f`, then it tends to `𝓝 (Filter.limUnder f g)`. We formulate +/-- If `g` tends to some `𝓝 x` along `f`, then it tends to `𝓝 (Filter.limUnder f g)`. We formulate this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for types without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance. -/ -theorem tendsto_nhds_limUnder {f : Filter Ξ±} {g : Ξ± β†’ X} (h : βˆƒ a, Tendsto g f (𝓝 a)) : +theorem tendsto_nhds_limUnder {f : Filter Ξ±} {g : Ξ± β†’ X} (h : βˆƒ x, Tendsto g f (𝓝 x)) : Tendsto g f (𝓝 (@limUnder _ _ _ (nonempty_of_exists h) f g)) := le_nhds_lim h #align tendsto_nhds_lim tendsto_nhds_limUnder @@ -1628,21 +1628,22 @@ set_option quotPrecheck false in scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " tβ‚‚ "]" => @Continuous _ _ t₁ tβ‚‚ -theorem continuous_def {_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X β†’ Y} : - Continuous f ↔ βˆ€ s, IsOpen s β†’ IsOpen (f ⁻¹' s) := +variable {f : X β†’ Y} {s : Set X} {x : X} {y : Y} + +theorem continuous_def : Continuous f ↔ βˆ€ s, IsOpen s β†’ IsOpen (f ⁻¹' s) := ⟨fun hf => hf.1, fun h => ⟨h⟩⟩ #align continuous_def continuous_def -theorem IsOpen.preimage {f : X β†’ Y} (hf : Continuous f) {s : Set Y} (h : IsOpen s) : - IsOpen (f ⁻¹' s) := - hf.isOpen_preimage s h +theorem IsOpen.preimage (hf : Continuous f) {t : Set Y} (h : IsOpen t) : + IsOpen (f ⁻¹' t) := + hf.isOpen_preimage t h #align is_open.preimage IsOpen.preimage -theorem continuous_congr {f g : X β†’ Y} (h : βˆ€ x, f x = g x) : +theorem continuous_congr {g : X β†’ Y} (h : βˆ€ x, f x = g x) : Continuous f ↔ Continuous g := .of_eq <| congrArg _ <| funext h -theorem Continuous.congr {f g : X β†’ Y} (h : Continuous f) (h' : βˆ€ x, f x = g x) : Continuous g := +theorem Continuous.congr {g : X β†’ Y} (h : Continuous f) (h' : βˆ€ x, f x = g x) : Continuous g := continuous_congr h' |>.mp h #align continuous.congr Continuous.congr @@ -1652,47 +1653,47 @@ def ContinuousAt (f : X β†’ Y) (x : X) := Tendsto f (𝓝 x) (𝓝 (f x)) #align continuous_at ContinuousAt -theorem ContinuousAt.tendsto {f : X β†’ Y} {x : X} (h : ContinuousAt f x) : +theorem ContinuousAt.tendsto (h : ContinuousAt f x) : Tendsto f (𝓝 x) (𝓝 (f x)) := h #align continuous_at.tendsto ContinuousAt.tendsto -theorem continuousAt_def {f : X β†’ Y} {x : X} : ContinuousAt f x ↔ βˆ€ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x := +theorem continuousAt_def : ContinuousAt f x ↔ βˆ€ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x := Iff.rfl #align continuous_at_def continuousAt_def -theorem continuousAt_congr {f g : X β†’ Y} {x : X} (h : f =αΆ [𝓝 x] g) : +theorem continuousAt_congr {g : X β†’ Y} (h : f =αΆ [𝓝 x] g) : ContinuousAt f x ↔ ContinuousAt g x := by simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds] #align continuous_at_congr continuousAt_congr -theorem ContinuousAt.congr {f g : X β†’ Y} {x : X} (hf : ContinuousAt f x) (h : f =αΆ [𝓝 x] g) : +theorem ContinuousAt.congr {g : X β†’ Y} (hf : ContinuousAt f x) (h : f =αΆ [𝓝 x] g) : ContinuousAt g x := (continuousAt_congr h).1 hf #align continuous_at.congr ContinuousAt.congr -theorem ContinuousAt.preimage_mem_nhds {f : X β†’ Y} {x : X} {t : Set Y} (h : ContinuousAt f x) +theorem ContinuousAt.preimage_mem_nhds {t : Set Y} (h : ContinuousAt f x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x := h ht #align continuous_at.preimage_mem_nhds ContinuousAt.preimage_mem_nhds /-- Deprecated, please use `not_mem_tsupport_iff_eventuallyEq` instead. -/ @[deprecated] -- 15 January 2024 -theorem eventuallyEq_zero_nhds {Mβ‚€} [Zero Mβ‚€] {a : X} {f : X β†’ Mβ‚€} : - f =αΆ [𝓝 a] 0 ↔ a βˆ‰ closure (Function.support f) := by +theorem eventuallyEq_zero_nhds {Mβ‚€} [Zero Mβ‚€] {f : X β†’ Mβ‚€} : + f =αΆ [𝓝 x] 0 ↔ x βˆ‰ closure (Function.support f) := by rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds, Function.compl_support, EventuallyEq, eventually_iff] simp only [Pi.zero_apply] #align eventually_eq_zero_nhds eventuallyEq_zero_nhds -theorem ClusterPt.map {x : X} {la : Filter X} {lb : Filter Y} (H : ClusterPt x la) {f : X β†’ Y} - (hfc : ContinuousAt f x) (hf : Tendsto f la lb) : ClusterPt (f x) lb := +theorem ClusterPt.map {lx : Filter X} {ly : Filter Y} (H : ClusterPt x lx) + (hfc : ContinuousAt f x) (hf : Tendsto f lx ly) : ClusterPt (f x) ly := (NeBot.map H f).mono <| hfc.tendsto.inf hf #align cluster_pt.map ClusterPt.map /-- See also `interior_preimage_subset_preimage_interior`. -/ -theorem preimage_interior_subset_interior_preimage {f : X β†’ Y} {s : Set Y} (hf : Continuous f) : - f ⁻¹' interior s βŠ† interior (f ⁻¹' s) := +theorem preimage_interior_subset_interior_preimage {t : Set Y} (hf : Continuous f) : + f ⁻¹' interior t βŠ† interior (f ⁻¹' t) := interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf) #align preimage_interior_subset_interior_preimage preimage_interior_subset_interior_preimage @@ -1705,150 +1706,150 @@ theorem continuous_id : Continuous (id : X β†’ X) := @[continuity] theorem continuous_id' : Continuous (fun (x : X) => x) := continuous_id -theorem Continuous.comp {g : Y β†’ Z} {f : X β†’ Y} (hg : Continuous g) (hf : Continuous f) : +theorem Continuous.comp {g : Y β†’ Z} (hg : Continuous g) (hf : Continuous f) : Continuous (g ∘ f) := continuous_def.2 fun _ h => (h.preimage hg).preimage hf #align continuous.comp Continuous.comp -- This is needed due to reducibility issues with the `continuity` tactic. @[continuity] -theorem Continuous.comp' {g : Y β†’ Z} {f : X β†’ Y} (hg : Continuous g) (hf : Continuous f) : +theorem Continuous.comp' {g : Y β†’ Z} (hg : Continuous g) (hf : Continuous f) : Continuous (fun x => g (f x)) := hg.comp hf theorem Continuous.iterate {f : X β†’ X} (h : Continuous f) (n : β„•) : Continuous f^[n] := Nat.recOn n continuous_id fun _ ihn => ihn.comp h #align continuous.iterate Continuous.iterate -nonrec theorem ContinuousAt.comp {g : Y β†’ Z} {f : X β†’ Y} {x : X} (hg : ContinuousAt g (f x)) +nonrec theorem ContinuousAt.comp {g : Y β†’ Z} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x := hg.comp hf #align continuous_at.comp ContinuousAt.comp /-- See note [comp_of_eq lemmas] -/ -theorem ContinuousAt.comp_of_eq {g : Y β†’ Z} {f : X β†’ Y} {x : X} {y : Y} (hg : ContinuousAt g y) +theorem ContinuousAt.comp_of_eq {g : Y β†’ Z} (hg : ContinuousAt g y) (hf : ContinuousAt f x) (hy : f x = y) : ContinuousAt (g ∘ f) x := by subst hy; exact hg.comp hf #align continuous_at.comp_of_eq ContinuousAt.comp_of_eq -theorem Continuous.tendsto {f : X β†’ Y} (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) := +theorem Continuous.tendsto (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) := ((nhds_basis_opens x).tendsto_iff <| nhds_basis_opens <| f x).2 fun t ⟨hxt, ht⟩ => ⟨f ⁻¹' t, ⟨hxt, ht.preimage hf⟩, Subset.rfl⟩ #align continuous.tendsto Continuous.tendsto /-- A version of `Continuous.tendsto` that allows one to specify a simpler form of the limit. E.g., one can write `continuous_exp.tendsto' 0 1 exp_zero`. -/ -theorem Continuous.tendsto' {f : X β†’ Y} (hf : Continuous f) (x : X) (y : Y) (h : f x = y) : +theorem Continuous.tendsto' (hf : Continuous f) (x : X) (y : Y) (h : f x = y) : Tendsto f (𝓝 x) (𝓝 y) := h β–Έ hf.tendsto x #align continuous.tendsto' Continuous.tendsto' -theorem Continuous.continuousAt {f : X β†’ Y} {x : X} (h : Continuous f) : ContinuousAt f x := +theorem Continuous.continuousAt (h : Continuous f) : ContinuousAt f x := h.tendsto x #align continuous.continuous_at Continuous.continuousAt -theorem continuous_iff_continuousAt {f : X β†’ Y} : Continuous f ↔ βˆ€ x, ContinuousAt f x := +theorem continuous_iff_continuousAt : Continuous f ↔ βˆ€ x, ContinuousAt f x := ⟨Continuous.tendsto, fun hf => continuous_def.2 fun _U hU => isOpen_iff_mem_nhds.2 fun x hx => hf x <| hU.mem_nhds hx⟩ #align continuous_iff_continuous_at continuous_iff_continuousAt -theorem continuousAt_const {x : X} {b : Y} : ContinuousAt (fun _ : X => b) x := +theorem continuousAt_const : ContinuousAt (fun _ : X => y) x := tendsto_const_nhds #align continuous_at_const continuousAt_const @[continuity] -theorem continuous_const {b : Y} : Continuous fun _ : X => b := +theorem continuous_const : Continuous fun _ : X => y := continuous_iff_continuousAt.mpr fun _ => continuousAt_const #align continuous_const continuous_const -theorem Filter.EventuallyEq.continuousAt {x : X} {f : X β†’ Y} {y : Y} (h : f =αΆ [𝓝 x] fun _ => y) : +theorem Filter.EventuallyEq.continuousAt (h : f =αΆ [𝓝 x] fun _ => y) : ContinuousAt f x := (continuousAt_congr h).2 tendsto_const_nhds #align filter.eventually_eq.continuous_at Filter.EventuallyEq.continuousAt -theorem continuous_of_const {f : X β†’ Y} (h : βˆ€ x y, f x = f y) : Continuous f := +theorem continuous_of_const (h : βˆ€ x y, f x = f y) : Continuous f := continuous_iff_continuousAt.mpr fun x => Filter.EventuallyEq.continuousAt <| eventually_of_forall fun y => h y x #align continuous_of_const continuous_of_const -theorem continuousAt_id {x : X} : ContinuousAt id x := +theorem continuousAt_id : ContinuousAt id x := continuous_id.continuousAt #align continuous_at_id continuousAt_id -theorem ContinuousAt.iterate {f : X β†’ X} {x : X} (hf : ContinuousAt f x) (hx : f x = x) (n : β„•) : +theorem ContinuousAt.iterate {f : X β†’ X} (hf : ContinuousAt f x) (hx : f x = x) (n : β„•) : ContinuousAt f^[n] x := Nat.recOn n continuousAt_id fun n ihn => show ContinuousAt (f^[n] ∘ f) x from ContinuousAt.comp (hx.symm β–Έ ihn) hf #align continuous_at.iterate ContinuousAt.iterate -theorem continuous_iff_isClosed {f : X β†’ Y} : Continuous f ↔ βˆ€ s, IsClosed s β†’ IsClosed (f ⁻¹' s) := +theorem continuous_iff_isClosed : Continuous f ↔ βˆ€ s, IsClosed s β†’ IsClosed (f ⁻¹' s) := continuous_def.trans <| compl_surjective.forall.trans <| by simp only [isOpen_compl_iff, preimage_compl] #align continuous_iff_is_closed continuous_iff_isClosed -theorem IsClosed.preimage {f : X β†’ Y} (hf : Continuous f) {s : Set Y} (h : IsClosed s) : - IsClosed (f ⁻¹' s) := - continuous_iff_isClosed.mp hf s h +theorem IsClosed.preimage (hf : Continuous f) {t : Set Y} (h : IsClosed t) : + IsClosed (f ⁻¹' t) := + continuous_iff_isClosed.mp hf t h #align is_closed.preimage IsClosed.preimage -theorem mem_closure_image {f : X β†’ Y} {x : X} {s : Set X} (hf : ContinuousAt f x) +theorem mem_closure_image (hf : ContinuousAt f x) (hx : x ∈ closure s) : f x ∈ closure (f '' s) := mem_closure_of_frequently_of_tendsto ((mem_closure_iff_frequently.1 hx).mono fun _ => mem_image_of_mem _) hf #align mem_closure_image mem_closure_image -theorem continuousAt_iff_ultrafilter {f : X β†’ Y} {x} : +theorem continuousAt_iff_ultrafilter : ContinuousAt f x ↔ βˆ€ g : Ultrafilter X, ↑g ≀ 𝓝 x β†’ Tendsto f g (𝓝 (f x)) := tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x)) #align continuous_at_iff_ultrafilter continuousAt_iff_ultrafilter -theorem continuous_iff_ultrafilter {f : X β†’ Y} : +theorem continuous_iff_ultrafilter : Continuous f ↔ βˆ€ (x) (g : Ultrafilter X), ↑g ≀ 𝓝 x β†’ Tendsto f g (𝓝 (f x)) := by simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter] #align continuous_iff_ultrafilter continuous_iff_ultrafilter -theorem Continuous.closure_preimage_subset {f : X β†’ Y} (hf : Continuous f) (t : Set Y) : +theorem Continuous.closure_preimage_subset (hf : Continuous f) (t : Set Y) : closure (f ⁻¹' t) βŠ† f ⁻¹' closure t := by rw [← (isClosed_closure.preimage hf).closure_eq] exact closure_mono (preimage_mono subset_closure) #align continuous.closure_preimage_subset Continuous.closure_preimage_subset -theorem Continuous.frontier_preimage_subset {f : X β†’ Y} (hf : Continuous f) (t : Set Y) : +theorem Continuous.frontier_preimage_subset (hf : Continuous f) (t : Set Y) : frontier (f ⁻¹' t) βŠ† f ⁻¹' frontier t := diff_subset_diff (hf.closure_preimage_subset t) (preimage_interior_subset_interior_preimage hf) #align continuous.frontier_preimage_subset Continuous.frontier_preimage_subset /-- If a continuous map `f` maps `s` to `t`, then it maps `closure s` to `closure t`. -/ -protected theorem Set.MapsTo.closure {s : Set X} {t : Set Y} {f : X β†’ Y} (h : MapsTo f s t) +protected theorem Set.MapsTo.closure {t : Set Y} (h : MapsTo f s t) (hc : Continuous f) : MapsTo f (closure s) (closure t) := by simp only [MapsTo, mem_closure_iff_clusterPt] exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h) #align set.maps_to.closure Set.MapsTo.closure /-- See also `IsClosedMap.closure_image_eq_of_continuous`. -/ -theorem image_closure_subset_closure_image {f : X β†’ Y} {s : Set X} (h : Continuous f) : +theorem image_closure_subset_closure_image (h : Continuous f) : f '' closure s βŠ† closure (f '' s) := ((mapsTo_image f s).closure h).image_subset #align image_closure_subset_closure_image image_closure_subset_closure_image -- porting note: new lemma -theorem closure_image_closure {f : X β†’ Y} {s : Set X} (h : Continuous f) : +theorem closure_image_closure (h : Continuous f) : closure (f '' closure s) = closure (f '' s) := Subset.antisymm (closure_minimal (image_closure_subset_closure_image h) isClosed_closure) (closure_mono <| image_subset _ subset_closure) -theorem closure_subset_preimage_closure_image {f : X β†’ Y} {s : Set X} (h : Continuous f) : +theorem closure_subset_preimage_closure_image (h : Continuous f) : closure s βŠ† f ⁻¹' closure (f '' s) := by rw [← Set.image_subset_iff] exact image_closure_subset_closure_image h #align closure_subset_preimage_closure_image closure_subset_preimage_closure_image -theorem map_mem_closure {s : Set X} {t : Set Y} {f : X β†’ Y} {a : X} (hf : Continuous f) - (ha : a ∈ closure s) (ht : MapsTo f s t) : f a ∈ closure t := - ht.closure hf ha +theorem map_mem_closure {t : Set Y} (hf : Continuous f) + (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t := + ht.closure hf hx #align map_mem_closure map_mem_closure /-- If a continuous map `f` maps `s` to a closed set `t`, then it maps `closure s` to `t`. -/ -theorem Set.MapsTo.closure_left {s : Set X} {t : Set Y} {f : X β†’ Y} (h : MapsTo f s t) +theorem Set.MapsTo.closure_left {t : Set Y} (h : MapsTo f s t) (hc : Continuous f) (ht : IsClosed t) : MapsTo f (closure s) t := ht.closure_eq β–Έ h.closure hc #align set.maps_to.closure_left Set.MapsTo.closure_left @@ -1865,7 +1866,7 @@ variable {Ξ± ΞΉ : Type*} (f : Ξ± β†’ X) (g : X β†’ Y) def DenseRange := Dense (range f) #align dense_range DenseRange -variable {f} +variable {f : Ξ± β†’ X} {s : Set X} /-- A surjective map has dense range. -/ theorem Function.Surjective.denseRange (hf : Function.Surjective f) : DenseRange f := fun x => by @@ -1884,33 +1885,33 @@ theorem DenseRange.closure_range (h : DenseRange f) : closure (range f) = univ : h.closure_eq #align dense_range.closure_range DenseRange.closure_range -theorem Dense.denseRange_val {s : Set X} (h : Dense s) : DenseRange ((↑) : s β†’ X) := by +theorem Dense.denseRange_val (h : Dense s) : DenseRange ((↑) : s β†’ X) := by simpa only [DenseRange, Subtype.range_coe_subtype] #align dense.dense_range_coe Dense.denseRange_val -theorem Continuous.range_subset_closure_image_dense {f : X β†’ Y} (hf : Continuous f) {s : Set X} +theorem Continuous.range_subset_closure_image_dense {f : X β†’ Y} (hf : Continuous f) (hs : Dense s) : range f βŠ† closure (f '' s) := by rw [← image_univ, ← hs.closure_eq] exact image_closure_subset_closure_image hf #align continuous.range_subset_closure_image_dense Continuous.range_subset_closure_image_dense /-- The image of a dense set under a continuous map with dense range is a dense set. -/ -theorem DenseRange.dense_image {f : X β†’ Y} (hf' : DenseRange f) (hf : Continuous f) {s : Set X} +theorem DenseRange.dense_image {f : X β†’ Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) : Dense (f '' s) := (hf'.mono <| hf.range_subset_closure_image_dense hs).of_closure #align dense_range.dense_image DenseRange.dense_image /-- If `f` has dense range and `s` is an open set in the codomain of `f`, then the image of the preimage of `s` under `f` is dense in `s`. -/ -theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) {s : Set X} - (hs : IsOpen s) : s βŠ† closure (f '' (f ⁻¹' s)) := by +theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) (hs : IsOpen s) : + s βŠ† closure (f '' (f ⁻¹' s)) := by rw [image_preimage_eq_inter_range] exact hf.open_subset_closure_inter hs #align dense_range.subset_closure_image_preimage_of_is_open DenseRange.subset_closure_image_preimage_of_isOpen /-- If a continuous map with dense range maps a dense set to a subset of `t`, then `t` is a dense set. -/ -theorem DenseRange.dense_of_mapsTo {f : X β†’ Y} (hf' : DenseRange f) (hf : Continuous f) {s : Set X} +theorem DenseRange.dense_of_mapsTo {f : X β†’ Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {t : Set Y} (ht : MapsTo f s t) : Dense t := (hf'.dense_image hf hs).mono ht.image_subset #align dense_range.dense_of_maps_to DenseRange.dense_of_mapsTo @@ -1931,19 +1932,19 @@ theorem DenseRange.nonempty [h : Nonempty X] (hf : DenseRange f) : Nonempty Ξ± : hf.nonempty_iff.mpr h #align dense_range.nonempty DenseRange.nonempty -/-- Given a function `f : X β†’ Y` with dense range and `b : Y`, returns some `a : X`. -/ -def DenseRange.some (hf : DenseRange f) (b : X) : Ξ± := - Classical.choice <| hf.nonempty_iff.mpr ⟨b⟩ +/-- Given a function `f : X β†’ Y` with dense range and `y : Y`, returns some `x : X`. -/ +def DenseRange.some (hf : DenseRange f) (x : X) : Ξ± := + Classical.choice <| hf.nonempty_iff.mpr ⟨x⟩ #align dense_range.some DenseRange.some -nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) {s : Set X} (ho : IsOpen s) - (hs : s.Nonempty) : βˆƒ a, f a ∈ s := +nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) (ho : IsOpen s) (hs : s.Nonempty) : + βˆƒ a, f a ∈ s := exists_range_iff.1 <| hf.exists_mem_open ho hs #align dense_range.exists_mem_open DenseRange.exists_mem_open -theorem DenseRange.mem_nhds (h : DenseRange f) {b : X} {U : Set X} (U_in : U ∈ 𝓝 b) : - βˆƒ a, f a ∈ U := - let ⟨a, ha⟩ := h.exists_mem_open isOpen_interior ⟨b, mem_interior_iff_mem_nhds.2 U_in⟩ +theorem DenseRange.mem_nhds (h : DenseRange f) (hs : s ∈ 𝓝 x) : + βˆƒ a, f a ∈ s := + let ⟨a, ha⟩ := h.exists_mem_open isOpen_interior ⟨x, mem_interior_iff_mem_nhds.2 hs⟩ ⟨a, interior_subset ha⟩ #align dense_range.mem_nhds DenseRange.mem_nhds diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index bcae50c87539e..2fb2985994d43 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -1199,12 +1199,12 @@ def C1 := C ∩ {f | f (term I ho) = true} theorem isClosed_C0 : IsClosed (C0 C ho) := by refine hC.inter ?_ have h : Continuous (fun (f : I β†’ Bool) ↦ f (term I ho)) := continuous_apply (term I ho) - exact IsClosed.preimage h (s := {false}) (isClosed_discrete _) + exact IsClosed.preimage h (t := {false}) (isClosed_discrete _) theorem isClosed_C1 : IsClosed (C1 C ho) := by refine hC.inter ?_ have h : Continuous (fun (f : I β†’ Bool) ↦ f (term I ho)) := continuous_apply (term I ho) - exact IsClosed.preimage h (s := {true}) (isClosed_discrete _) + exact IsClosed.preimage h (t := {true}) (isClosed_discrete _) theorem contained_C1 : contained (Ο€ (C1 C ho) (ord I Β· < o)) o := contained_proj _ _ diff --git a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean index 8c14400addc73..a44f4d1ddb383 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean @@ -1177,7 +1177,7 @@ theorem closure_subset_thickening {Ξ΄ : ℝ} (Ξ΄_pos : 0 < Ξ΄) (E : Set Ξ±) : /-- A set is contained in its own (open) thickening. -/ theorem self_subset_thickening {Ξ΄ : ℝ} (Ξ΄_pos : 0 < Ξ΄) (E : Set Ξ±) : E βŠ† thickening Ξ΄ E := - (@subset_closure _ _ E).trans (closure_subset_thickening Ξ΄_pos E) + (@subset_closure _ E).trans (closure_subset_thickening Ξ΄_pos E) #align metric.self_subset_thickening Metric.self_subset_thickening /-- A set is contained in its own closed thickening. -/ diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean index f72a9118ee9f8..dd9b26cdc66ca 100644 --- a/Mathlib/Topology/Order.lean +++ b/Mathlib/Topology/Order.lean @@ -243,11 +243,11 @@ theorem IsOpen.mono (hs : IsOpen[tβ‚‚] s) (h : t₁ ≀ tβ‚‚) : IsOpen[t₁] s : #align is_open.mono IsOpen.mono theorem IsClosed.mono (hs : IsClosed[tβ‚‚] s) (h : t₁ ≀ tβ‚‚) : IsClosed[t₁] s := - (@isOpen_compl_iff Ξ± t₁ s).mp <| hs.isOpen_compl.mono h + (@isOpen_compl_iff Ξ± s t₁).mp <| hs.isOpen_compl.mono h #align is_closed.mono IsClosed.mono theorem closure.mono (h : t₁ ≀ tβ‚‚) : closure[t₁] s βŠ† closure[tβ‚‚] s := - @closure_minimal _ t₁ s (@closure _ tβ‚‚ s) subset_closure (IsClosed.mono isClosed_closure h) + @closure_minimal _ s (@closure _ tβ‚‚ s) t₁ subset_closure (IsClosed.mono isClosed_closure h) theorem isOpen_implies_isOpen_iff : (βˆ€ s, IsOpen[t₁] s β†’ IsOpen[tβ‚‚] s) ↔ tβ‚‚ ≀ t₁ := Iff.rfl @@ -313,7 +313,7 @@ theorem mem_nhds_discrete {x : Ξ±} {s : Set Ξ±} : end DiscreteTopology theorem le_of_nhds_le_nhds (h : βˆ€ x, @nhds Ξ± t₁ x ≀ @nhds Ξ± tβ‚‚ x) : t₁ ≀ tβ‚‚ := fun s => by - rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds Ξ± tβ‚‚] + rw [@isOpen_iff_mem_nhds _ _ t₁, @isOpen_iff_mem_nhds Ξ± _ tβ‚‚] exact fun hs a ha => h _ (hs _ ha) #align le_of_nhds_le_nhds le_of_nhds_le_nhds @@ -1024,7 +1024,7 @@ theorem isOpen_iSup_iff {s : Set Ξ±} : IsOpen[⨆ i, t i] s ↔ βˆ€ i, IsOpen[t #align is_open_supr_iff isOpen_iSup_iff theorem isClosed_iSup_iff {s : Set Ξ±} : IsClosed[⨆ i, t i] s ↔ βˆ€ i, IsClosed[t i] s := by - simp [← @isOpen_compl_iff _ (⨆ i, t i), ← @isOpen_compl_iff _ (t _), isOpen_iSup_iff] + simp [← @isOpen_compl_iff _ _ (⨆ i, t i), ← @isOpen_compl_iff _ _ (t _), isOpen_iSup_iff] #align is_closed_supr_iff isClosed_iSup_iff end iInf diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index ca3285c191eee..c1ea2809b87d2 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -1810,12 +1810,12 @@ theorem isOpen_of_uniformity_sum_aux {s : Set (Sum Ξ± Ξ²)} { p : (Ξ± βŠ• Ξ²) Γ— (Ξ± βŠ• Ξ²) | p.1 = x β†’ p.2 ∈ s } ∈ (@UniformSpace.Core.sum Ξ± Ξ² _ _).uniformity) : IsOpen s := by constructor - Β· refine' (@isOpen_iff_mem_nhds Ξ± _ _).2 fun a ha => mem_nhds_uniformity_iff_right.2 _ + Β· refine (isOpen_iff_mem_nhds (X := Ξ±)).2 fun a ha ↦ mem_nhds_uniformity_iff_right.2 ?_ rcases mem_map_iff_exists_image.1 (hs _ ha).1 with ⟨t, ht, st⟩ refine' mem_of_superset ht _ rintro p pt rfl exact st ⟨_, pt, rfl⟩ rfl - Β· refine' (@isOpen_iff_mem_nhds Ξ² _ _).2 fun b hb => mem_nhds_uniformity_iff_right.2 _ + Β· refine (@isOpen_iff_mem_nhds (X := Ξ²)).2 fun b hb ↦ mem_nhds_uniformity_iff_right.2 ?_ rcases mem_map_iff_exists_image.1 (hs _ hb).2 with ⟨t, ht, st⟩ refine' mem_of_superset ht _ rintro p pt rfl diff --git a/Mathlib/Topology/UniformSpace/CompactConvergence.lean b/Mathlib/Topology/UniformSpace/CompactConvergence.lean index 87c07e30fd68d..ae784a173bc48 100644 --- a/Mathlib/Topology/UniformSpace/CompactConvergence.lean +++ b/Mathlib/Topology/UniformSpace/CompactConvergence.lean @@ -271,7 +271,7 @@ theorem compactOpen_eq_compactConvergence : Β· refine' fun X hX => isOpen_iff_forall_mem_open.mpr fun f hf => _ have hXf : X ∈ (compactConvergenceFilterBasis f).filter := by rw [← nhds_compactConvergence] - exact @IsOpen.mem_nhds C(Ξ±, Ξ²) compactConvergenceTopology _ _ hX hf + exact @IsOpen.mem_nhds C(Ξ±, Ξ²) _ _ compactConvergenceTopology hX hf obtain ⟨-, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hXf⟩ := hXf obtain ⟨ι, hΞΉ, C, hC, U, hU, h₁, hβ‚‚βŸ© := iInter_compactOpen_gen_subset_compactConvNhd f hK hV haveI := hΞΉ