diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean index 29a3e37e415e9..918b1807523fb 100644 --- a/Mathlib/AlgebraicGeometry/Limits.lean +++ b/Mathlib/AlgebraicGeometry/Limits.lean @@ -96,7 +96,7 @@ instance (priority := 100) isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X ⟶ · apply openEmbedding_of_continuous_injective_open · continuity · rintro (i : X.carrier); exact isEmptyElim i - · intro U _; convert isOpen_empty (α := Y); ext; rw [Set.mem_empty_iff_false, iff_false_iff] + · intro U _; convert isOpen_empty (X := Y); ext; rw [Set.mem_empty_iff_false, iff_false_iff] exact fun x => isEmptyElim (show X.carrier from x.choose) · rintro (i : X.carrier); exact isEmptyElim i #align algebraic_geometry.is_open_immersion_of_is_empty AlgebraicGeometry.isOpenImmersion_of_isEmpty diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean index 861dedace3e67..4f4c3d8d2614e 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean @@ -642,7 +642,7 @@ theorem localization_comap_inducing [Algebra R S] (M : Submonoid R) [IsLocalizat constructor rw [TopologicalSpace.ext_iff] intro U - rw [← isClosed_compl_iff, ← @isClosed_compl_iff (α := PrimeSpectrum S) (s := U)] + rw [← isClosed_compl_iff, ← @isClosed_compl_iff (X := PrimeSpectrum S) (s := U)] generalize Uᶜ = Z simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus] constructor diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean index 88c23a19a310e..c9a2a657eda95 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean @@ -390,7 +390,7 @@ theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) tauto have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := continuous_ofReal.continuousAt.prod_map continuousAt_id - exact ContinuousAt.comp (α := ℝ × ℂ) (f := fun p => ⟨↑p.1, p.2⟩) (x := ⟨0, y⟩) A B + exact A.comp_of_eq B rfl · -- x < 0 : difficult case suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _) diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 75192b66184b9..7569c2c1bfd94 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean @@ -1658,14 +1658,10 @@ theorem _root_.Embedding.aestronglyMeasurable_comp_iff [PseudoMetrizableSpace β refine' ⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨_, _⟩, fun H => hg.continuous.comp_aestronglyMeasurable H⟩ - · let G : β → range g := codRestrict g (range g) mem_range_self + · let G : β → range g := rangeFactorization g have hG : ClosedEmbedding G := { hg.codRestrict _ _ with - closed_range := by - convert isClosed_univ (α := ↥(range g)) - apply eq_univ_of_forall - rintro ⟨-, ⟨x, rfl⟩⟩ - exact mem_range_self x } + closed_range := by rw [surjective_onto_range.range_eq]; exact isClosed_univ } have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this · rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩ diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index 23a6b5c68250c..e8f00715ed372 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -1028,10 +1028,8 @@ theorem tendsto_sum_nat_add [T2Space α] (f : ℕ → α) : rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf] have h₁ : Tendsto (fun _ : ℕ => ∑' i, f i) atTop (𝓝 (∑' i, f i)) := tendsto_const_nhds simpa only [h₀, sub_self] using Tendsto.sub h₁ hf.hasSum.tendsto_sum_nat - · convert tendsto_const_nhds (α := α) (β := ℕ) (a := 0) (f := atTop) - rename_i i - rw [← summable_nat_add_iff i] at hf - exact tsum_eq_zero_of_not_summable hf + · refine tendsto_const_nhds.congr fun n ↦ (tsum_eq_zero_of_not_summable ?_).symm + rwa [summable_nat_add_iff n] #align tendsto_sum_nat_add tendsto_sum_nat_add /-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both convergent then so is the `ℤ`-indexed @@ -1317,8 +1315,7 @@ theorem tendsto_tsum_compl_atTop_zero (f : α → G) : obtain ⟨s, hs⟩ := H.tsum_vanishing he rw [Filter.mem_map, mem_atTop_sets] exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩ - · convert tendsto_const_nhds (α := G) (β := Finset α) (f := atTop) (a := 0) - apply tsum_eq_zero_of_not_summable + · refine tendsto_const_nhds.congr fun _ ↦ (tsum_eq_zero_of_not_summable ?_).symm rwa [Finset.summable_compl_iff] #align tendsto_tsum_compl_at_top_zero tendsto_tsum_compl_atTop_zero diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index b1418ad62b6e9..9b702e014ce5f 100644 --- a/Mathlib/Topology/Basic.lean +++ b/Mathlib/Topology/Basic.lean @@ -13,14 +13,14 @@ import Mathlib.Tactic.Continuity /-! # Basic theory of topological spaces. -The main definition is the type class `TopologicalSpace α` which endows a type `α` with a topology. -Then `Set α` gets predicates `IsOpen`, `IsClosed` and functions `interior`, `closure` and -`frontier`. Each point `x` of `α` gets a neighborhood filter `𝓝 x`. A filter `F` on `α` has -`x` as a cluster point if `ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥`. A map `f : ι → α` clusters at `x` -along `F : Filter ι` if `MapClusterPt x F f : ClusterPt x (map f F)`. In particular +The main definition is the type class `TopologicalSpace X` which endows a type `X` with a topology. +Then `Set X` gets predicates `IsOpen`, `IsClosed` and functions `interior`, `closure` and +`frontier`. Each point `x` of `X` gets a neighborhood filter `𝓝 x`. A filter `F` on `X` has +`x` as a cluster point if `ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥`. A map `f : α → X` clusters at `x` +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 `α` and `β`, a function `f : α → β` and a point `a : α`, +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 `Continuous f`. There is also a version of continuity `PContinuous` for partially defined functions. @@ -55,18 +55,18 @@ noncomputable section open Set Filter -universe u v w +universe u v w x /-! ### Topological spaces -/ -/-- A topology on `α`. -/ +/-- A topology on `X`. -/ @[to_additive existing TopologicalSpace] -class TopologicalSpace (α : Type u) where +class TopologicalSpace (X : Type u) where /-- A predicate saying that a set is an open set. Use `IsOpen` in the root namespace instead. -/ - protected IsOpen : Set α → Prop + protected IsOpen : Set X → Prop /-- The set representing the whole space is an open set. Use `isOpen_univ` in the root namespace instead. -/ protected isOpen_univ : IsOpen univ @@ -79,9 +79,9 @@ class TopologicalSpace (α : Type u) where /-- A constructor for topologies by specifying the closed sets, and showing that they satisfy the appropriate conditions. -/ -def TopologicalSpace.ofClosed {α : Type u} (T : Set (Set α)) (empty_mem : ∅ ∈ T) +def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : ∅ ∈ T) (sInter_mem : ∀ A, A ⊆ T → ⋂₀ A ∈ T) - (union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T) : TopologicalSpace α where + (union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T) : TopologicalSpace X where IsOpen X := Xᶜ ∈ T isOpen_univ := by simp [empty_mem] isOpen_inter s t hs ht := by simpa only [compl_inter] using union_mem sᶜ hs tᶜ ht @@ -92,10 +92,11 @@ def TopologicalSpace.ofClosed {α : Type u} (T : Set (Set α)) (empty_mem : ∅ section TopologicalSpace -variable {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ t : Set α} {p p₁ p₂ : α → Prop} +variable {X : Type u} {Y : Type v} {ι : Sort w} {α β : Type*} + {a : 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 `α` -/ -def IsOpen [TopologicalSpace α] : Set α → Prop := TopologicalSpace.IsOpen +/-- `IsOpen s` means that `s` is open in the ambient topological space on `X` -/ +def IsOpen [TopologicalSpace X] : Set X → Prop := TopologicalSpace.IsOpen #align is_open IsOpen set_option quotPrecheck false in @@ -104,48 +105,48 @@ scoped[Topology] notation (name := IsOpen_of) "IsOpen[" t "]" => @IsOpen _ t open Topology -lemma isOpen_mk {p h₁ h₂ h₃} {s : Set α} : IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s := Iff.rfl +lemma isOpen_mk {p h₁ h₂ h₃} {s : Set X} : IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s := Iff.rfl #align is_open_mk isOpen_mk @[ext] protected theorem TopologicalSpace.ext : - ∀ {f g : TopologicalSpace α}, IsOpen[f] = IsOpen[g] → f = g + ∀ {f g : TopologicalSpace X}, IsOpen[f] = IsOpen[g] → f = g | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl #align topological_space_eq TopologicalSpace.ext section -variable [TopologicalSpace α] +variable [TopologicalSpace X] -@[simp] theorem isOpen_univ : IsOpen (univ : Set α) := TopologicalSpace.isOpen_univ +@[simp] theorem isOpen_univ : IsOpen (univ : Set X) := TopologicalSpace.isOpen_univ #align is_open_univ isOpen_univ theorem IsOpen.inter (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∩ s₂) := TopologicalSpace.isOpen_inter s₁ s₂ h₁ h₂ #align is_open.inter IsOpen.inter -theorem isOpen_sUnion {s : Set (Set α)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s) := +theorem isOpen_sUnion {s : Set (Set X)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s) := TopologicalSpace.isOpen_sUnion s h #align is_open_sUnion isOpen_sUnion end -protected theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace α} : +protected theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace X} : t = t' ↔ ∀ s, IsOpen[t] s ↔ IsOpen[t'] s := ⟨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 α} {t : TopologicalSpace α} : t.IsOpen s = IsOpen[t] s := +theorem isOpen_fold {s : Set X} {t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s := rfl #align is_open_fold isOpen_fold -variable [TopologicalSpace α] +variable [TopologicalSpace X] -theorem isOpen_iUnion {f : ι → Set α} (h : ∀ i, IsOpen (f i)) : IsOpen (⋃ i, f i) := +theorem isOpen_iUnion {f : ι → Set X} (h : ∀ i, IsOpen (f i)) : IsOpen (⋃ i, f i) := isOpen_sUnion (forall_range_iff.2 h) #align is_open_Union isOpen_iUnion -theorem isOpen_biUnion {s : Set β} {f : β → Set α} (h : ∀ i ∈ s, IsOpen (f i)) : +theorem isOpen_biUnion {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋃ i ∈ s, f i) := isOpen_iUnion fun i => isOpen_iUnion fun hi => h i hi #align is_open_bUnion isOpen_biUnion @@ -154,41 +155,41 @@ theorem IsOpen.union (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ rw [union_eq_iUnion]; exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩) #align is_open.union IsOpen.union -lemma isOpen_iff_of_cover {ι : Type*} {f : ι → Set α} (ho : ∀ i, IsOpen (f i)) - (hU : (⋃ i, f i) = univ) : IsOpen s ↔ ∀ i, IsOpen (f i ∩ s) := by +lemma isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) : + IsOpen s ↔ ∀ i, IsOpen (f i ∩ s) := by refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩ rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter] exact isOpen_iUnion fun i ↦ h i -@[simp] theorem isOpen_empty : IsOpen (∅ : Set α) := by +@[simp] theorem isOpen_empty : IsOpen (∅ : Set X) := by rw [← sUnion_empty]; exact isOpen_sUnion fun a => False.elim #align is_open_empty isOpen_empty -theorem Set.Finite.isOpen_sInter {s : Set (Set α)} (hs : s.Finite) : +theorem Set.Finite.isOpen_sInter {s : Set (Set X)} (hs : s.Finite) : (∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s) := Finite.induction_on hs (fun _ => by rw [sInter_empty]; exact isOpen_univ) fun _ _ ih h => by simp only [sInter_insert, ball_insert_iff] at h ⊢ exact h.1.inter (ih h.2) #align is_open_sInter Set.Finite.isOpen_sInter -theorem Set.Finite.isOpen_biInter {s : Set β} {f : β → Set α} (hs : s.Finite) +theorem Set.Finite.isOpen_biInter {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i) := sInter_image f s ▸ (hs.image _).isOpen_sInter (ball_image_iff.2 h) #align is_open_bInter Set.Finite.isOpen_biInter -theorem isOpen_iInter_of_finite [Finite ι] {s : ι → Set α} (h : ∀ i, IsOpen (s i)) : +theorem isOpen_iInter_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsOpen (s i)) : IsOpen (⋂ i, s i) := (finite_range _).isOpen_sInter (forall_range_iff.2 h) #align is_open_Inter isOpen_iInter_of_finite -theorem isOpen_biInter_finset {s : Finset β} {f : β → Set α} (h : ∀ i ∈ s, IsOpen (f i)) : +theorem isOpen_biInter_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i) := s.finite_toSet.isOpen_biInter h #align is_open_bInter_finset isOpen_biInter_finset @[simp] -- porting note: added `simp` -theorem isOpen_const {p : Prop} : IsOpen { _a : α | p } := by by_cases p <;> simp [*] +theorem isOpen_const {p : Prop} : IsOpen { _a : 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 } := @@ -196,7 +197,7 @@ theorem IsOpen.and : IsOpen { a | p₁ a } → IsOpen { a | p₂ a } → IsOpen #align is_open.and IsOpen.and /-- A set is closed if its complement is open -/ -class IsClosed (s : Set α) : Prop where +class IsClosed (s : Set X) : Prop where /-- The complement of a closed set is an open set. -/ isOpen_compl : IsOpen sᶜ #align is_closed IsClosed @@ -205,45 +206,45 @@ 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 α} : IsOpen sᶜ ↔ IsClosed s := +@[simp] theorem isOpen_compl_iff {s : Set X} : IsOpen sᶜ ↔ IsClosed s := ⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩ #align is_open_compl_iff isOpen_compl_iff -- porting note: new lemma -theorem isClosed_const {p : Prop} : IsClosed { _a : α | p } := ⟨isOpen_const (p := ¬p)⟩ +theorem isClosed_const {p : Prop} : IsClosed { _a : X | p } := ⟨isOpen_const (p := ¬p)⟩ -@[simp] theorem isClosed_empty : IsClosed (∅ : Set α) := isClosed_const +@[simp] theorem isClosed_empty : IsClosed (∅ : Set X) := isClosed_const #align is_closed_empty isClosed_empty -@[simp] theorem isClosed_univ : IsClosed (univ : Set α) := isClosed_const +@[simp] theorem isClosed_univ : IsClosed (univ : Set X) := isClosed_const #align is_closed_univ isClosed_univ theorem IsClosed.union : IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂) := by simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter #align is_closed.union IsClosed.union -theorem isClosed_sInter {s : Set (Set α)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s) := by +theorem isClosed_sInter {s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s) := by simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion #align is_closed_sInter isClosed_sInter -theorem isClosed_iInter {f : ι → Set α} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i) := +theorem isClosed_iInter {f : ι → Set X} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i) := isClosed_sInter <| forall_range_iff.2 h #align is_closed_Inter isClosed_iInter -theorem isClosed_biInter {s : Set β} {f : β → Set α} (h : ∀ i ∈ s, IsClosed (f i)) : +theorem isClosed_biInter {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋂ i ∈ s, f i) := isClosed_iInter fun i => isClosed_iInter <| h i #align is_closed_bInter isClosed_biInter @[simp] -theorem isClosed_compl_iff {s : Set α} : IsClosed sᶜ ↔ IsOpen s := by +theorem isClosed_compl_iff {s : Set X} : IsClosed sᶜ ↔ IsOpen s := by rw [← isOpen_compl_iff, compl_compl] #align is_closed_compl_iff isClosed_compl_iff alias ⟨_, IsOpen.isClosed_compl⟩ := isClosed_compl_iff #align is_open.is_closed_compl IsOpen.isClosed_compl -theorem IsOpen.sdiff {s t : Set α} (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t) := +theorem IsOpen.sdiff {s t : Set X} (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t) := IsOpen.inter h₁ h₂.isOpen_compl #align is_open.sdiff IsOpen.sdiff @@ -253,28 +254,28 @@ 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 α} (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t) := +theorem IsClosed.sdiff {s t : Set X} (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t) := IsClosed.inter h₁ (isClosed_compl_iff.mpr h₂) #align is_closed.sdiff IsClosed.sdiff -theorem Set.Finite.isClosed_biUnion {s : Set β} {f : β → Set α} (hs : s.Finite) +theorem Set.Finite.isClosed_biUnion {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋃ i ∈ s, f i) := by simp only [← isOpen_compl_iff, compl_iUnion] at * exact hs.isOpen_biInter h #align is_closed_bUnion Set.Finite.isClosed_biUnion -lemma isClosed_biUnion_finset {s : Finset β} {f : β → Set α} (h : ∀ i ∈ s, IsClosed (f i)) : +lemma isClosed_biUnion_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋃ i ∈ s, f i) := s.finite_toSet.isClosed_biUnion h -theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set α} (h : ∀ i, IsClosed (s i)) : +theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsClosed (s i)) : IsClosed (⋃ i, s i) := by simp only [← isOpen_compl_iff, compl_iUnion] at * exact isOpen_iInter_of_finite h #align is_closed_Union isClosed_iUnion_of_finite -theorem isClosed_imp {p q : α → Prop} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) : +theorem isClosed_imp {p q : X → Prop} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) : IsClosed { x | p x → q x } := by simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq #align is_closed_imp isClosed_imp @@ -288,45 +289,45 @@ theorem IsClosed.not : IsClosed { a | p a } → IsOpen { a | ¬p a } := -/ /-- The interior of a set `s` is the largest open subset of `s`. -/ -def interior (s : Set α) : Set α := +def interior (s : Set X) : Set X := ⋃₀ { t | IsOpen t ∧ t ⊆ s } #align interior interior -- porting note: use `∃ t, t ⊆ s ∧ _` instead of `∃ t ⊆ s, _` -theorem mem_interior {s : Set α} {x : α} : x ∈ interior s ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := by +theorem mem_interior {s : Set X} {x : X} : 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 α} : IsOpen (interior s) := +theorem isOpen_interior {s : Set X} : IsOpen (interior s) := isOpen_sUnion fun _ => And.left #align is_open_interior isOpen_interior -theorem interior_subset {s : Set α} : interior s ⊆ s := +theorem interior_subset {s : Set X} : interior s ⊆ s := sUnion_subset fun _ => And.right #align interior_subset interior_subset -theorem interior_maximal {s t : Set α} (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s := +theorem interior_maximal {s t : Set X} (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 α} (h : IsOpen s) : interior s = s := +theorem IsOpen.interior_eq {s : Set X} (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 α} : interior s = s ↔ IsOpen s := +theorem interior_eq_iff_isOpen {s : Set X} : 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 α} : s ⊆ interior s ↔ IsOpen s := by +theorem subset_interior_iff_isOpen {s : Set X} : 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 α} (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t := +theorem IsOpen.subset_interior_iff {s t : Set X} (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 α} : t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s := +theorem subset_interior_iff {s t : Set X} : 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 @@ -335,58 +336,58 @@ lemma interior_subset_iff : interior s ⊆ t ↔ ∀ U, IsOpen U → U ⊆ s → simp [interior] @[mono] -theorem interior_mono {s t : Set α} (h : s ⊆ t) : interior s ⊆ interior t := +theorem interior_mono {s t : Set X} (h : s ⊆ t) : interior s ⊆ interior t := interior_maximal (Subset.trans interior_subset h) isOpen_interior #align interior_mono interior_mono @[simp] -theorem interior_empty : interior (∅ : Set α) = ∅ := +theorem interior_empty : interior (∅ : Set X) = ∅ := isOpen_empty.interior_eq #align interior_empty interior_empty @[simp] -theorem interior_univ : interior (univ : Set α) = univ := +theorem interior_univ : interior (univ : Set X) = univ := isOpen_univ.interior_eq #align interior_univ interior_univ @[simp] -theorem interior_eq_univ {s : Set α} : interior s = univ ↔ s = univ := +theorem interior_eq_univ {s : Set X} : 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 α} : interior (interior s) = interior s := +theorem interior_interior {s : Set X} : interior (interior s) = interior s := isOpen_interior.interior_eq #align interior_interior interior_interior @[simp] -theorem interior_inter {s t : Set α} : interior (s ∩ t) = interior s ∩ interior t := +theorem interior_inter {s t : Set X} : 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 #align interior_inter interior_inter -theorem Set.Finite.interior_biInter {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set α) : +theorem Set.Finite.interior_biInter {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) : interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) := hs.induction_on (by simp) <| by intros; simp [*] -theorem Set.Finite.interior_sInter {S : Set (Set α)} (hS : S.Finite) : +theorem Set.Finite.interior_sInter {S : Set (Set X)} (hS : S.Finite) : interior (⋂₀ S) = ⋂ s ∈ S, interior s := by rw [sInter_eq_biInter, hS.interior_biInter] @[simp] -theorem Finset.interior_iInter {ι : Type*} (s : Finset ι) (f : ι → Set α) : +theorem Finset.interior_iInter {ι : Type*} (s : Finset ι) (f : ι → Set X) : interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) := s.finite_toSet.interior_biInter f #align finset.interior_Inter Finset.interior_iInter @[simp] -theorem interior_iInter_of_finite [Finite ι] (f : ι → Set α) : +theorem interior_iInter_of_finite [Finite ι] (f : ι → Set X) : interior (⋂ i, f i) = ⋂ i, interior (f i) := by 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 α} (h₁ : IsClosed s) +theorem interior_union_isClosed_of_interior_empty {s t : Set X} (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 => @@ -402,16 +403,16 @@ theorem isOpen_iff_forall_mem_open : IsOpen s ↔ ∀ x ∈ s, ∃ t, t ⊆ s simp only [subset_def, mem_interior] #align is_open_iff_forall_mem_open isOpen_iff_forall_mem_open -theorem interior_iInter_subset (s : ι → Set α) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) := +theorem interior_iInter_subset (s : ι → Set X) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) := subset_iInter fun _ => interior_mono <| iInter_subset _ _ #align interior_Inter_subset interior_iInter_subset -theorem interior_iInter₂_subset (p : ι → Sort*) (s : ∀ i, p i → Set α) : +theorem interior_iInter₂_subset (p : ι → Sort*) (s : ∀ i, p i → Set X) : interior (⋂ (i) (j), s i j) ⊆ ⋂ (i) (j), interior (s i j) := (interior_iInter_subset _).trans <| iInter_mono fun _ => interior_iInter_subset _ #align interior_Inter₂_subset interior_iInter₂_subset -theorem interior_sInter_subset (S : Set (Set α)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s := +theorem interior_sInter_subset (S : Set (Set X)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s := calc interior (⋂₀ S) = interior (⋂ s ∈ S, s) := by rw [sInter_eq_biInter] _ ⊆ ⋂ s ∈ S, interior s := interior_iInter₂_subset _ _ @@ -423,7 +424,7 @@ theorem interior_sInter_subset (S : Set (Set α)) : interior (⋂₀ S) ⊆ ⋂ /-- The closure of `s` is the smallest closed set containing `s`. -/ -def closure (s : Set α) : Set α := +def closure (s : Set X) : Set X := ⋂₀ { t | IsClosed t ∧ s ⊆ t } #align closure closure @@ -432,91 +433,91 @@ set_option quotPrecheck false in scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t @[simp] -theorem isClosed_closure {s : Set α} : IsClosed (closure s) := +theorem isClosed_closure {s : Set X} : IsClosed (closure s) := isClosed_sInter fun _ => And.left #align is_closed_closure isClosed_closure -theorem subset_closure {s : Set α} : s ⊆ closure s := +theorem subset_closure {s : Set X} : s ⊆ closure s := subset_sInter fun _ => And.right #align subset_closure subset_closure -theorem not_mem_of_not_mem_closure {s : Set α} {P : α} (hP : P ∉ closure s) : P ∉ s := fun h => +theorem not_mem_of_not_mem_closure {s : Set X} {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 α} (h₁ : s ⊆ t) (h₂ : IsClosed t) : closure s ⊆ t := +theorem closure_minimal {s t : Set X} (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 α} (hd : Disjoint s t) (ht : IsOpen t) : +theorem Disjoint.closure_left {s t : Set X} (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 α} (hd : Disjoint s t) (hs : IsOpen s) : +theorem Disjoint.closure_right {s t : Set X} (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 α} (h : IsClosed s) : closure s = s := +theorem IsClosed.closure_eq {s : Set X} (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 α} (hs : IsClosed s) : closure s ⊆ s := +theorem IsClosed.closure_subset {s : Set X} (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 α} (h₁ : IsClosed t) : closure s ⊆ t ↔ s ⊆ t := +theorem IsClosed.closure_subset_iff {s t : Set X} (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 α} (hs : IsClosed s) {x : α} : - x ∈ s ↔ closure ({x} : Set α) ⊆ s := +theorem IsClosed.mem_iff_closure_subset {s : Set X} (hs : IsClosed s) {x : X} : + 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 α} (h : s ⊆ t) : closure s ⊆ closure t := +theorem closure_mono {s t : Set X} (h : s ⊆ t) : closure s ⊆ closure t := closure_minimal (Subset.trans h subset_closure) isClosed_closure #align closure_mono closure_mono -theorem monotone_closure (α : Type*) [TopologicalSpace α] : Monotone (@closure α _) := fun _ _ => +theorem monotone_closure (X : Type*) [TopologicalSpace X] : Monotone (@closure X _) := fun _ _ => closure_mono #align monotone_closure monotone_closure -theorem diff_subset_closure_iff {s t : Set α} : s \ t ⊆ closure t ↔ s ⊆ closure t := by +theorem diff_subset_closure_iff {s t : Set X} : 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 -theorem closure_inter_subset_inter_closure (s t : Set α) : +theorem closure_inter_subset_inter_closure (s t : Set X) : closure (s ∩ t) ⊆ closure s ∩ closure t := - (monotone_closure α).map_inf_le s t + (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 α} (h : closure s ⊆ s) : IsClosed s := by +theorem isClosed_of_closure_subset {s : Set X} (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 α} : closure s = s ↔ IsClosed s := +theorem closure_eq_iff_isClosed {s : Set X} : 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 α} : closure s ⊆ s ↔ IsClosed s := +theorem closure_subset_iff_isClosed {s : Set X} : closure s ⊆ s ↔ IsClosed s := ⟨isClosed_of_closure_subset, IsClosed.closure_subset⟩ #align closure_subset_iff_is_closed closure_subset_iff_isClosed @[simp] -theorem closure_empty : closure (∅ : Set α) = ∅ := +theorem closure_empty : closure (∅ : Set X) = ∅ := isClosed_empty.closure_eq #align closure_empty closure_empty @[simp] -theorem closure_empty_iff (s : Set α) : closure s = ∅ ↔ s = ∅ := +theorem closure_empty_iff (s : Set X) : closure s = ∅ ↔ s = ∅ := ⟨subset_eq_empty subset_closure, fun h => h.symm ▸ closure_empty⟩ #align closure_empty_iff closure_empty_iff @[simp] -theorem closure_nonempty_iff {s : Set α} : (closure s).Nonempty ↔ s.Nonempty := by +theorem closure_nonempty_iff {s : Set X} : (closure s).Nonempty ↔ s.Nonempty := by simp only [nonempty_iff_ne_empty, Ne.def, closure_empty_iff] #align closure_nonempty_iff closure_nonempty_iff @@ -525,60 +526,60 @@ alias ⟨Set.Nonempty.of_closure, Set.Nonempty.closure⟩ := closure_nonempty_if #align set.nonempty.closure Set.Nonempty.closure @[simp] -theorem closure_univ : closure (univ : Set α) = univ := +theorem closure_univ : closure (univ : Set X) = univ := isClosed_univ.closure_eq #align closure_univ closure_univ @[simp] -theorem closure_closure {s : Set α} : closure (closure s) = closure s := +theorem closure_closure {s : Set X} : closure (closure s) = closure s := isClosed_closure.closure_eq #align closure_closure closure_closure -theorem closure_eq_compl_interior_compl {s : Set α} : closure s = (interior sᶜ)ᶜ := by +theorem closure_eq_compl_interior_compl {s : Set X} : 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 α} : closure (s ∪ t) = closure s ∪ closure t := by +theorem closure_union {s t : Set X} : closure (s ∪ t) = closure s ∪ closure t := by simp [closure_eq_compl_interior_compl, compl_inter] #align closure_union closure_union -theorem Set.Finite.closure_biUnion {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set α) : +theorem Set.Finite.closure_biUnion {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) : closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) := by simp [closure_eq_compl_interior_compl, hs.interior_biInter] -theorem Set.Finite.closure_sUnion {S : Set (Set α)} (hS : S.Finite) : +theorem Set.Finite.closure_sUnion {S : Set (Set X)} (hS : S.Finite) : closure (⋃₀ S) = ⋃ s ∈ S, closure s := by rw [sUnion_eq_biUnion, hS.closure_biUnion] @[simp] -theorem Finset.closure_biUnion {ι : Type*} (s : Finset ι) (f : ι → Set α) : +theorem Finset.closure_biUnion {ι : Type*} (s : Finset ι) (f : ι → Set X) : closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) := s.finite_toSet.closure_biUnion f #align finset.closure_bUnion Finset.closure_biUnion @[simp] -theorem closure_iUnion_of_finite [Finite ι] (f : ι → Set α) : +theorem closure_iUnion_of_finite [Finite ι] (f : ι → Set X) : closure (⋃ i, f i) = ⋃ i, closure (f i) := by rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range] #align closure_Union closure_iUnion_of_finite -theorem interior_subset_closure {s : Set α} : interior s ⊆ closure s := +theorem interior_subset_closure {s : Set X} : interior s ⊆ closure s := Subset.trans interior_subset subset_closure #align interior_subset_closure interior_subset_closure @[simp] -theorem interior_compl {s : Set α} : interior sᶜ = (closure s)ᶜ := by +theorem interior_compl {s : Set X} : interior sᶜ = (closure s)ᶜ := by simp [closure_eq_compl_interior_compl] #align interior_compl interior_compl @[simp] -theorem closure_compl {s : Set α} : closure sᶜ = (interior s)ᶜ := by +theorem closure_compl {s : Set X} : closure sᶜ = (interior s)ᶜ := by simp [closure_eq_compl_interior_compl] #align closure_compl closure_compl -theorem mem_closure_iff {s : Set α} {a : α} : +theorem mem_closure_iff {s : Set X} {a : X} : a ∈ closure s ↔ ∀ o, IsOpen o → a ∈ o → (o ∩ s).Nonempty := ⟨fun h o oo ao => by_contradiction fun os => @@ -590,56 +591,56 @@ theorem mem_closure_iff {s : Set α} {a : α} : hc (h₂ hs)⟩ #align mem_closure_iff mem_closure_iff -theorem closure_inter_open_nonempty_iff {s t : Set α} (h : IsOpen t) : +theorem closure_inter_open_nonempty_iff {s t : Set X} (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⟩ #align closure_inter_open_nonempty_iff closure_inter_open_nonempty_iff -theorem Filter.le_lift'_closure (l : Filter α) : l ≤ l.lift' closure := +theorem Filter.le_lift'_closure (l : Filter X) : l ≤ l.lift' closure := le_lift'.2 fun _ h => mem_of_superset h subset_closure #align filter.le_lift'_closure Filter.le_lift'_closure -theorem Filter.HasBasis.lift'_closure {l : Filter α} {p : ι → Prop} {s : ι → Set α} +theorem Filter.HasBasis.lift'_closure {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) : (l.lift' closure).HasBasis p fun i => closure (s i) := - h.lift' (monotone_closure α) + h.lift' (monotone_closure X) #align filter.has_basis.lift'_closure Filter.HasBasis.lift'_closure -theorem Filter.HasBasis.lift'_closure_eq_self {l : Filter α} {p : ι → Prop} {s : ι → Set α} +theorem Filter.HasBasis.lift'_closure_eq_self {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) (hc : ∀ i, p i → IsClosed (s i)) : l.lift' closure = l := le_antisymm (h.ge_iff.2 fun i hi => (hc i hi).closure_eq ▸ mem_lift' (h.mem_of_mem hi)) l.le_lift'_closure #align filter.has_basis.lift'_closure_eq_self Filter.HasBasis.lift'_closure_eq_self @[simp] -theorem Filter.lift'_closure_eq_bot {l : Filter α} : l.lift' closure = ⊥ ↔ l = ⊥ := +theorem Filter.lift'_closure_eq_bot {l : Filter X} : l.lift' closure = ⊥ ↔ l = ⊥ := ⟨fun h => bot_unique <| h ▸ l.le_lift'_closure, fun h => h.symm ▸ by rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]⟩ #align filter.lift'_closure_eq_bot Filter.lift'_closure_eq_bot /-- A set is dense in a topological space if every point belongs to its closure. -/ -def Dense (s : Set α) : Prop := +def Dense (s : Set X) : Prop := ∀ x, x ∈ closure s #align dense Dense -theorem dense_iff_closure_eq {s : Set α} : Dense s ↔ closure s = univ := +theorem dense_iff_closure_eq {s : Set X} : 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 α} : interior s = ∅ ↔ Dense sᶜ := by +theorem interior_eq_empty_iff_dense_compl {s : Set X} : 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 α} (h : Dense s) : interior sᶜ = ∅ := +theorem Dense.interior_compl {s : Set X} (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 α} : Dense (closure s) ↔ Dense s := by +theorem dense_closure {s : Set X} : Dense (closure s) ↔ Dense s := by rw [Dense, Dense, closure_closure] #align dense_closure dense_closure @@ -649,11 +650,11 @@ alias ⟨Dense.of_closure, _⟩ := dense_closure #align dense.closure Dense.closure @[simp] -theorem dense_univ : Dense (univ : Set α) := fun _ => subset_closure trivial +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 α} : +theorem dense_iff_inter_open {s : Set X} : Dense s ↔ ∀ U, IsOpen U → U.Nonempty → (U ∩ s).Nonempty := by constructor <;> intro h · rintro U U_op ⟨x, x_in⟩ @@ -667,30 +668,30 @@ theorem dense_iff_inter_open {s : Set α} : 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 α} (hs : Dense s) {U : Set α} (ho : IsOpen U) +theorem Dense.exists_mem_open {s : Set X} (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 α} (hs : Dense s) : s.Nonempty ↔ Nonempty α := +theorem Dense.nonempty_iff {s : Set X} (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 α] {s : Set α} (hs : Dense s) : s.Nonempty := +theorem Dense.nonempty [h : Nonempty X] {s : Set X} (hs : Dense s) : s.Nonempty := hs.nonempty_iff.2 h #align dense.nonempty Dense.nonempty @[mono] -theorem Dense.mono {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (hd : Dense s₁) : Dense s₂ := fun x => +theorem Dense.mono {s₁ s₂ : Set X} (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 : α} : - Dense ({x}ᶜ : Set α) ↔ ¬IsOpen ({x} : Set α) := by +theorem dense_compl_singleton_iff_not_open {x : X} : + Dense ({x}ᶜ : Set X) ↔ ¬IsOpen ({x} : Set X) := by constructor · intro hd ho exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _) @@ -705,12 +706,12 @@ theorem dense_compl_singleton_iff_not_open {x : α} : -/ /-- The frontier of a set is the set of points between the closure and interior. -/ -def frontier (s : Set α) : Set α := +def frontier (s : Set X) : Set X := closure s \ interior s #align frontier frontier @[simp] -theorem closure_diff_interior (s : Set α) : closure s \ interior s = frontier s := +theorem closure_diff_interior (s : Set X) : closure s \ interior s = frontier s := rfl #align closure_diff_interior closure_diff_interior @@ -720,21 +721,21 @@ lemma disjoint_interior_frontier : Disjoint (interior s) (frontier s) := by ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter] @[simp] -theorem closure_diff_frontier (s : Set α) : closure s \ frontier s = interior s := by +theorem closure_diff_frontier (s : Set X) : closure s \ frontier s = interior s := by rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure] #align closure_diff_frontier closure_diff_frontier @[simp] -theorem self_diff_frontier (s : Set α) : s \ frontier s = interior s := by +theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s := by rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure, 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 α} : frontier s = closure s ∩ closure sᶜ := by +theorem frontier_eq_closure_inter_closure {s : Set X} : 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 α} : frontier s ⊆ closure s := +theorem frontier_subset_closure {s : Set X} : frontier s ⊆ closure s := diff_subset _ _ #align frontier_subset_closure frontier_subset_closure @@ -742,59 +743,59 @@ 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 α} : frontier (closure s) ⊆ frontier s := +theorem frontier_closure_subset {s : Set X} : 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 α} : frontier (interior s) ⊆ frontier s := +theorem frontier_interior_subset {s : Set X} : frontier (interior s) ⊆ frontier s := diff_subset_diff (closure_mono interior_subset) interior_interior.symm.subset #align frontier_interior_subset frontier_interior_subset /-- The complement of a set has the same frontier as the original set. -/ @[simp] -theorem frontier_compl (s : Set α) : frontier sᶜ = frontier s := by +theorem frontier_compl (s : Set X) : frontier sᶜ = frontier s := by simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm] #align frontier_compl frontier_compl @[simp] -theorem frontier_univ : frontier (univ : Set α) = ∅ := by simp [frontier] +theorem frontier_univ : frontier (univ : Set X) = ∅ := by simp [frontier] #align frontier_univ frontier_univ @[simp] -theorem frontier_empty : frontier (∅ : Set α) = ∅ := by simp [frontier] +theorem frontier_empty : frontier (∅ : Set X) = ∅ := by simp [frontier] #align frontier_empty frontier_empty -theorem frontier_inter_subset (s t : Set α) : +theorem frontier_inter_subset (s t : Set X) : frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t := by simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union] refine' (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq _ simp only [inter_distrib_left, inter_distrib_right, inter_assoc, inter_comm (closure t)] #align frontier_inter_subset frontier_inter_subset -theorem frontier_union_subset (s t : Set α) : +theorem frontier_union_subset (s t : Set X) : frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t := by 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 α} (hs : IsClosed s) : frontier s = s \ interior s := by +theorem IsClosed.frontier_eq {s : Set X} (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 α} (hs : IsOpen s) : frontier s = closure s \ s := by +theorem IsOpen.frontier_eq {s : Set X} (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 α} (hs : IsOpen s) : s ∩ frontier s = ∅ := by +theorem IsOpen.inter_frontier_eq {s : Set X} (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 α} : IsClosed (frontier s) := by +theorem isClosed_frontier {s : Set X} : 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 α} (h : IsClosed s) : interior (frontier s) = ∅ := by +theorem interior_frontier {s : Set X} (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 @@ -803,11 +804,11 @@ theorem interior_frontier {s : Set α} (h : IsClosed s) : interior (frontier s) rwa [inter_diff_self, subset_empty_iff] at this #align interior_frontier interior_frontier -theorem closure_eq_interior_union_frontier (s : Set α) : closure s = interior s ∪ frontier s := +theorem closure_eq_interior_union_frontier (s : Set X) : closure s = interior s ∪ frontier s := (union_diff_cancel interior_subset_closure).symm #align closure_eq_interior_union_frontier closure_eq_interior_union_frontier -theorem closure_eq_self_union_frontier (s : Set α) : closure s = s ∪ frontier s := +theorem closure_eq_self_union_frontier (s : Set X) : closure s = s ∪ frontier s := (union_diff_cancel' interior_subset subset_closure).symm #align closure_eq_self_union_frontier closure_eq_self_union_frontier @@ -820,12 +821,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 α} : +theorem frontier_eq_inter_compl_interior {s : Set X} : 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 α} : +theorem compl_frontier_eq_union_interior {s : Set X} : (frontier s)ᶜ = interior s ∪ interior sᶜ := by rw [frontier_eq_inter_compl_interior] simp only [compl_inter, compl_compl] @@ -838,14 +839,14 @@ theorem compl_frontier_eq_union_interior {s : Set α} : /-- 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 : α) : Filter α := - ⨅ s ∈ { s : Set α | a ∈ s ∧ IsOpen s }, 𝓟 s +irreducible_def nhds (a : X) : Filter X := + ⨅ s ∈ { s : Set X | a ∈ 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 : α) (s : Set α) : Filter α := +def nhdsWithin (a : X) (s : Set X) : Filter X := nhds a ⊓ 𝓟 s #align nhds_within nhdsWithin @@ -874,14 +875,14 @@ scoped[Topology] notation3 "𝓝[<] " x:100 => nhdsWithin x (Set.Iio x) end -theorem nhds_def' (a : α) : 𝓝 a = ⨅ (s : Set α) (_ : IsOpen s) (_ : a ∈ s), 𝓟 s := by +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] #align nhds_def' nhds_def' /-- The open sets containing `a` are a basis for the neighborhood filter. See `nhds_basis_opens'` for a variant using open neighborhoods instead. -/ -theorem nhds_basis_opens (a : α) : - (𝓝 a).HasBasis (fun s : Set α => a ∈ s ∧ IsOpen s) fun s => s := by +theorem nhds_basis_opens (a : X) : + (𝓝 a).HasBasis (fun s : Set X => a ∈ s ∧ IsOpen s) fun s => s := by rw [nhds_def] exact hasBasis_biInf_principal (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ => @@ -889,114 +890,114 @@ theorem nhds_basis_opens (a : α) : ⟨univ, ⟨mem_univ a, isOpen_univ⟩⟩ #align nhds_basis_opens nhds_basis_opens -theorem nhds_basis_closeds (a : α) : (𝓝 a).HasBasis (fun s : Set α => a ∉ s ∧ IsClosed s) compl := +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 <| 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 α, a ∈ s → IsOpen s → s ∈ f := by simp [nhds_def] +theorem le_nhds_iff {f a} : f ≤ 𝓝 a ↔ ∀ s : Set X, a ∈ 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 α} (h : a ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 a ≤ f := by +theorem nhds_le_of_le {f a} {s : Set X} (h : a ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 a ≤ 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 : α} {s : Set α} : s ∈ 𝓝 a ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ a ∈ t := +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 _ => ⟨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 : α} {p : α → Prop} : - (∀ᶠ x in 𝓝 a, p x) ↔ ∃ t : Set α, (∀ x ∈ t, p x) ∧ IsOpen t ∧ a ∈ t := +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 := 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 α} {a : α} : a ∈ interior s ↔ s ∈ 𝓝 a := +theorem mem_interior_iff_mem_nhds {s : Set X} {a : X} : a ∈ interior s ↔ s ∈ 𝓝 a := mem_interior.trans mem_nhds_iff.symm #align mem_interior_iff_mem_nhds mem_interior_iff_mem_nhds -theorem map_nhds {a : α} {f : α → β} : - map f (𝓝 a) = ⨅ s ∈ { s : Set α | a ∈ s ∧ IsOpen s }, 𝓟 (image f s) := +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 #align map_nhds map_nhds -theorem mem_of_mem_nhds {a : α} {s : Set α} : s ∈ 𝓝 a → a ∈ s := fun H => +theorem mem_of_mem_nhds {a : X} {s : Set X} : s ∈ 𝓝 a → a ∈ 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 : α → Prop} {a : α} (h : ∀ᶠ y in 𝓝 a, p y) : p a := +theorem Filter.Eventually.self_of_nhds {p : X → Prop} {a : X} (h : ∀ᶠ y in 𝓝 a, p y) : p a := mem_of_mem_nhds h #align filter.eventually.self_of_nhds Filter.Eventually.self_of_nhds -theorem IsOpen.mem_nhds {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈ s) : s ∈ 𝓝 a := +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⟩ #align is_open.mem_nhds IsOpen.mem_nhds -protected theorem IsOpen.mem_nhds_iff {a : α} {s : Set α} (hs : IsOpen s) : s ∈ 𝓝 a ↔ a ∈ s := +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⟩⟩ #align is_open.mem_nhds_iff IsOpen.mem_nhds_iff -theorem IsClosed.compl_mem_nhds {a : α} {s : Set α} (hs : IsClosed s) (ha : a ∉ s) : sᶜ ∈ 𝓝 a := +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) #align is_closed.compl_mem_nhds IsClosed.compl_mem_nhds -theorem IsOpen.eventually_mem {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈ s) : +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 #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 : α) : - (𝓝 a).HasBasis (fun s : Set α => s ∈ 𝓝 a ∧ IsOpen s) fun x => x := by +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 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 α} (h : ∀ x ∈ s, U ∈ 𝓝 x) : - ∃ V : Set α, s ⊆ V ∧ IsOpen V ∧ V ⊆ U := +theorem exists_open_set_nhds {s 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 α} (h : U ∈ ⨆ x ∈ s, 𝓝 x) : - ∃ V : Set α, s ⊆ V ∧ IsOpen V ∧ V ⊆ U := +theorem exists_open_set_nhds' {s 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 : α → Prop} {a : α} (h : ∀ᶠ y in 𝓝 a, p 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 := 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 : α → Prop} {a : α} : +theorem eventually_eventually_nhds {p : X → Prop} {a : X} : (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝 a, 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 : α → Prop} {a : α} : +theorem frequently_frequently_nhds {p : X → Prop} {a : X} : (∃ᶠ y in 𝓝 a, ∃ᶠ x in 𝓝 y, p x) ↔ ∃ᶠ x in 𝓝 a, 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 α} {a : α} : (∀ᶠ x in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a := +theorem eventually_mem_nhds {s : Set X} {a : X} : (∀ᶠ x in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a := eventually_eventually_nhds #align eventually_mem_nhds eventually_mem_nhds @@ -1006,93 +1007,92 @@ theorem nhds_bind_nhds : (𝓝 a).bind 𝓝 = 𝓝 a := #align nhds_bind_nhds nhds_bind_nhds @[simp] -theorem eventually_eventuallyEq_nhds {f g : α → β} {a : α} : +theorem eventually_eventuallyEq_nhds {f g : X → α} {a : X} : (∀ᶠ y in 𝓝 a, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 a] g := eventually_eventually_nhds #align eventually_eventually_eq_nhds eventually_eventuallyEq_nhds -theorem Filter.EventuallyEq.eq_of_nhds {f g : α → β} {a : α} (h : f =ᶠ[𝓝 a] g) : f a = g a := +theorem Filter.EventuallyEq.eq_of_nhds {f g : X → α} {a : X} (h : f =ᶠ[𝓝 a] g) : f a = g a := h.self_of_nhds #align filter.eventually_eq.eq_of_nhds Filter.EventuallyEq.eq_of_nhds @[simp] -theorem eventually_eventuallyLE_nhds [LE β] {f g : α → β} {a : α} : +theorem eventually_eventuallyLE_nhds [LE α] {f g : X → α} {a : X} : (∀ᶠ y in 𝓝 a, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 a] 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 : α → β} {a : α} (h : f =ᶠ[𝓝 a] g) : +theorem Filter.EventuallyEq.eventuallyEq_nhds {f g : X → α} {a : X} (h : f =ᶠ[𝓝 a] g) : ∀ᶠ y in 𝓝 a, 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 `f x ≤ g x` in a neighbourhood of `y`. -/ -theorem Filter.EventuallyLE.eventuallyLE_nhds [LE β] {f g : α → β} {a : α} (h : f ≤ᶠ[𝓝 a] g) : +theorem Filter.EventuallyLE.eventuallyLE_nhds [LE α] {f g : X → α} {a : X} (h : f ≤ᶠ[𝓝 a] g) : ∀ᶠ y in 𝓝 a, f ≤ᶠ[𝓝 y] g := h.eventually_nhds #align filter.eventually_le.eventually_le_nhds Filter.EventuallyLE.eventuallyLE_nhds -theorem all_mem_nhds (x : α) (P : Set α → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) : +theorem all_mem_nhds (x : X) (P : Set X → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) : (∀ s ∈ 𝓝 x, P s) ↔ ∀ s, IsOpen s → x ∈ s → P s := ((nhds_basis_opens x).forall_iff hP).trans <| by simp only [@and_comm (x ∈ _), and_imp] #align all_mem_nhds all_mem_nhds -theorem all_mem_nhds_filter (x : α) (f : Set α → Set β) (hf : ∀ s t, s ⊆ t → f s ⊆ f t) - (l : Filter β) : (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l := +theorem all_mem_nhds_filter (x : X) (f : Set X → Set α) (hf : ∀ s t, s ⊆ t → f s ⊆ f t) + (l : Filter α) : (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l := 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 : β → α} {l : Filter β} {a : α} : +theorem tendsto_nhds {f : α → X} {l : Filter α} {a : X} : Tendsto f l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ 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 : β → α} {a : α} : - Tendsto f atTop (𝓝 a) ↔ ∀ U : Set α, a ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U := +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 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 : α} {f : Filter β} : Tendsto (fun _ : β => a) f (𝓝 a) := +theorem tendsto_const_nhds {a : X} {f : Filter α} : Tendsto (fun _ : α => a) f (𝓝 a) := 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 : α} - {u : ι → α} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Tendsto u atTop (𝓝 x) := +theorem tendsto_atTop_of_eventually_const {ι : Type*} [SemilatticeSup ι] [Nonempty ι] {x : X} + {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 : α} - {u : ι → α} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Tendsto u atBot (𝓝 x) := +theorem tendsto_atBot_of_eventually_const {ι : Type*} [SemilatticeInf ι] [Nonempty ι] {x : X} + {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 -theorem pure_le_nhds : pure ≤ (𝓝 : α → Filter α) := fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs +theorem pure_le_nhds : pure ≤ (𝓝 : X → Filter X) := fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs #align pure_le_nhds pure_le_nhds -theorem tendsto_pure_nhds {α : Type*} [TopologicalSpace β] (f : α → β) (a : α) : - Tendsto f (pure a) (𝓝 (f a)) := +theorem tendsto_pure_nhds (f : α → X) (a : α) : Tendsto f (pure a) (𝓝 (f a)) := (tendsto_pure_pure f a).mono_right (pure_le_nhds _) #align tendsto_pure_nhds tendsto_pure_nhds -theorem OrderTop.tendsto_atTop_nhds {α : Type*} [PartialOrder α] [OrderTop α] [TopologicalSpace β] - (f : α → β) : Tendsto f atTop (𝓝 (f ⊤)) := +theorem OrderTop.tendsto_atTop_nhds [PartialOrder α] [OrderTop α] (f : α → X) : + Tendsto f atTop (𝓝 (f ⊤)) := (tendsto_atTop_pure f).mono_right (pure_le_nhds _) #align order_top.tendsto_at_top_nhds OrderTop.tendsto_atTop_nhds @[simp] -instance nhds_neBot {a : α} : NeBot (𝓝 a) := +instance nhds_neBot {a : X} : NeBot (𝓝 a) := neBot_of_le (pure_le_nhds a) #align nhds_ne_bot nhds_neBot -theorem tendsto_nhds_of_eventually_eq {l : Filter β} {f : β → α} {a : α} (h : ∀ᶠ x in l, f x = a) : +theorem tendsto_nhds_of_eventually_eq {l : Filter α} {f : α → X} {a : X} (h : ∀ᶠ x in l, f x = a) : Tendsto f l (𝓝 a) := tendsto_const_nhds.congr' (.symm h) -theorem Filter.EventuallyEq.tendsto {l : Filter β} {f : β → α} {a : α} (hf : f =ᶠ[l] fun _ ↦ a) : +theorem Filter.EventuallyEq.tendsto {l : Filter α} {f : α → X} {a : X} (hf : f =ᶠ[l] fun _ ↦ a) : Tendsto f l (𝓝 a) := tendsto_nhds_of_eventually_eq hf @@ -1107,85 +1107,85 @@ In this section we define [cluster points](https://en.wikipedia.org/wiki/Limit_p /-- A point `x` is a cluster point of a filter `F` if `𝓝 x ⊓ F ≠ ⊥`. Also known as an accumulation point or a limit point, but beware that terminology varies. This is *not* the same as asking `𝓝[≠] x ⊓ F ≠ ⊥`. See `mem_closure_iff_clusterPt` in particular. -/ -def ClusterPt (x : α) (F : Filter α) : Prop := +def ClusterPt (x : X) (F : Filter X) : Prop := NeBot (𝓝 x ⊓ F) #align cluster_pt ClusterPt -theorem ClusterPt.neBot {x : α} {F : Filter α} (h : ClusterPt x F) : NeBot (𝓝 x ⊓ F) := +theorem ClusterPt.neBot {x : X} {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 α} {pF : ιF → Prop} - {sF : ιF → Set α} {F : Filter α} (ha : (𝓝 a).HasBasis pa sa) (hF : F.HasBasis pF sF) : +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 #align filter.has_basis.cluster_pt_iff Filter.HasBasis.clusterPt_iff -theorem clusterPt_iff {x : α} {F : Filter α} : - ClusterPt x F ↔ ∀ ⦃U : Set α⦄, U ∈ 𝓝 x → ∀ ⦃V⦄, V ∈ F → (U ∩ V).Nonempty := +theorem clusterPt_iff {x : X} {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 : α} {F : Filter α} : +theorem clusterPt_iff_not_disjoint {x : X} {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 : α} {s : Set α} : +theorem clusterPt_principal_iff {x : X} {s : Set X} : 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 : α} {s : Set α} : +theorem clusterPt_principal_iff_frequently {x : X} {s : Set X} : 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 : α} {f : Filter α} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f := by +theorem ClusterPt.of_le_nhds {x : X} {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 : α} {f : Filter α} (H : f ≤ 𝓝 x) (_hf : NeBot f) : +theorem ClusterPt.of_le_nhds' {x : X} {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 : α} {f : Filter α} (H : 𝓝 x ≤ f) : ClusterPt x f := by +theorem ClusterPt.of_nhds_le {x : X} {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 : α} {f g : Filter α} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g := +theorem ClusterPt.mono {x : X} {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 : α} {f g : Filter α} (H : ClusterPt x <| f ⊓ g) : ClusterPt x f := +theorem ClusterPt.of_inf_left {x : X} {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 : α} {f g : Filter α} (H : ClusterPt x <| f ⊓ g) : +theorem ClusterPt.of_inf_right {x : X} {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 : α} {f : Ultrafilter α} : ClusterPt x f ↔ ↑f ≤ 𝓝 x := +theorem Ultrafilter.clusterPt_iff {x : X} {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 /-- A point `x` is a cluster point of a sequence `u` along a filter `F` if it is a cluster point of `map u F`. -/ -def MapClusterPt {ι : Type*} (x : α) (F : Filter ι) (u : ι → α) : Prop := +def MapClusterPt {ι : Type*} (x : X) (F : Filter ι) (u : ι → X) : Prop := ClusterPt x (map u F) #align map_cluster_pt MapClusterPt -theorem mapClusterPt_iff {ι : Type*} (x : α) (F : Filter ι) (u : ι → α) : +theorem mapClusterPt_iff {ι : Type*} (x : X) (F : Filter ι) (u : ι → X) : MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ a in F, u a ∈ s := by simp_rw [MapClusterPt, ClusterPt, inf_neBot_iff_frequently_left, frequently_map] rfl #align map_cluster_pt_iff mapClusterPt_iff -theorem mapClusterPt_of_comp {ι δ : Type*} {F : Filter ι} {φ : δ → ι} {p : Filter δ} {x : α} - {u : ι → α} [NeBot p] (h : Tendsto φ p F) (H : Tendsto (u ∘ φ) p (𝓝 x)) : +theorem mapClusterPt_of_comp {F : Filter α} {φ : β → α} {p : Filter β} {x : X} + {u : α → X} [NeBot p] (h : Tendsto φ p F) (H : Tendsto (u ∘ φ) p (𝓝 x)) : MapClusterPt x F u := by have := calc @@ -1196,36 +1196,36 @@ theorem mapClusterPt_of_comp {ι δ : Type*} {F : Filter ι} {φ : δ → ι} {p #align map_cluster_pt_of_comp mapClusterPt_of_comp /-- A point `x` is an accumulation point of a filter `F` if `𝓝[≠] x ⊓ F ≠ ⊥`.-/ -def AccPt (x : α) (F : Filter α) : Prop := +def AccPt (x : X) (F : Filter X) : Prop := NeBot (𝓝[≠] x ⊓ F) #align acc_pt AccPt -theorem acc_iff_cluster (x : α) (F : Filter α) : AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F) := by +theorem acc_iff_cluster (x : X) (F : Filter X) : AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F) := by rw [AccPt, nhdsWithin, ClusterPt, inf_assoc] #align acc_iff_cluster acc_iff_cluster /-- `x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`.-/ -theorem acc_principal_iff_cluster (x : α) (C : Set α) : +theorem acc_principal_iff_cluster (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x})) := by rw [acc_iff_cluster, inf_principal, inter_comm, diff_eq] #align acc_principal_iff_cluster acc_principal_iff_cluster /-- `x` is an accumulation point of a set `C` iff every neighborhood of `x` contains a point of `C` other than `x`. -/ -theorem accPt_iff_nhds (x : α) (C : Set α) : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by +theorem accPt_iff_nhds (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by simp [acc_principal_iff_cluster, clusterPt_principal_iff, Set.Nonempty, exists_prop, and_assoc, @and_comm (¬_ = x)] #align acc_pt_iff_nhds accPt_iff_nhds /-- `x` is an accumulation point of a set `C` iff there are points near `x` in `C` and different from `x`.-/ -theorem accPt_iff_frequently (x : α) (C : Set α) : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C := by +theorem accPt_iff_frequently (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C := by simp [acc_principal_iff_cluster, clusterPt_principal_iff_frequently, and_comm] #align acc_pt_iff_frequently accPt_iff_frequently /-- If `x` is an accumulation point of `F` and `F ≤ G`, then `x` is an accumulation point of `D`. -/ -theorem AccPt.mono {x : α} {F G : Filter α} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G := +theorem AccPt.mono {x : X} {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 @@ -1233,53 +1233,53 @@ theorem AccPt.mono {x : α} {F G : Filter α} (h : AccPt x F) (hFG : F ≤ G) : ### Interior, closure and frontier in terms of neighborhoods -/ -theorem interior_eq_nhds' {s : Set α} : interior s = { a | s ∈ 𝓝 a } := +theorem interior_eq_nhds' {s : Set X} : interior s = { a | s ∈ 𝓝 a } := 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 α} : interior s = { a | 𝓝 a ≤ 𝓟 s } := +theorem interior_eq_nhds {s : Set X} : interior s = { a | 𝓝 a ≤ 𝓟 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 α} {a : α} : interior s ∈ 𝓝 a ↔ s ∈ 𝓝 a := +theorem interior_mem_nhds {s : Set X} {a : X} : interior s ∈ 𝓝 a ↔ s ∈ 𝓝 a := ⟨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 -theorem interior_setOf_eq {p : α → Prop} : interior { x | p x } = { x | ∀ᶠ y in 𝓝 x, p y } := +theorem interior_setOf_eq {p : X → Prop} : interior { x | p x } = { x | ∀ᶠ y in 𝓝 x, p y } := interior_eq_nhds' #align interior_set_of_eq interior_setOf_eq -theorem isOpen_setOf_eventually_nhds {p : α → Prop} : IsOpen { x | ∀ᶠ y in 𝓝 x, p y } := by +theorem isOpen_setOf_eventually_nhds {p : X → Prop} : IsOpen { x | ∀ᶠ y in 𝓝 x, p y } := by 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 α} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x := by +theorem subset_interior_iff_nhds {s 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 α} : IsOpen s ↔ ∀ a ∈ s, 𝓝 a ≤ 𝓟 s := +theorem isOpen_iff_nhds {s : Set X} : IsOpen s ↔ ∀ a ∈ s, 𝓝 a ≤ 𝓟 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] #align is_open_iff_nhds isOpen_iff_nhds -theorem isOpen_iff_mem_nhds {s : Set α} : IsOpen s ↔ ∀ a ∈ s, s ∈ 𝓝 a := +theorem isOpen_iff_mem_nhds {s : Set X} : IsOpen s ↔ ∀ a ∈ s, s ∈ 𝓝 a := 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 α} : IsOpen s ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, y ∈ s := +theorem isOpen_iff_eventually {s : Set X} : 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 α} : - IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l := by +theorem isOpen_iff_ultrafilter {s : Set X} : + 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 : α) : IsOpen ({a} : Set α) ↔ 𝓝 a = pure a := by +theorem isOpen_singleton_iff_nhds_eq_pure (a : X) : IsOpen ({a} : Set X) ↔ 𝓝 a = pure a := by constructor · intro h apply le_antisymm _ (pure_le_nhds a) @@ -1289,13 +1289,12 @@ theorem isOpen_singleton_iff_nhds_eq_pure (a : α) : IsOpen ({a} : Set α) ↔ 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 {α : Type*} [TopologicalSpace α] (a : α) : - IsOpen ({a} : Set α) ↔ 𝓝[≠] a = ⊥ := by +theorem isOpen_singleton_iff_punctured_nhds (a : X) : IsOpen ({a} : Set X) ↔ 𝓝[≠] a = ⊥ := 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 α} {a : α} : a ∈ closure s ↔ ∃ᶠ x in 𝓝 a, x ∈ s := by +theorem mem_closure_iff_frequently {s : Set X} {a : X} : a ∈ closure s ↔ ∃ᶠ x in 𝓝 a, 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 @@ -1305,7 +1304,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 α} : IsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s := by +theorem isClosed_iff_frequently {s : Set X} : 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] @@ -1313,30 +1312,30 @@ theorem isClosed_iff_frequently {s : Set α} : IsClosed s ↔ ∀ x, (∃ᶠ y i /-- The set of cluster points of a filter is closed. In particular, the set of limit points of a sequence is closed. -/ -theorem isClosed_setOf_clusterPt {f : Filter α} : IsClosed { x | ClusterPt x f } := by +theorem isClosed_setOf_clusterPt {f : Filter X} : IsClosed { x | ClusterPt x f } := by simp only [ClusterPt, inf_neBot_iff_frequently_left, setOf_forall, imp_iff_not_or] refine' isClosed_iInter fun p => IsClosed.union _ _ <;> apply isClosed_compl_iff.2 exacts [isOpen_setOf_eventually_nhds, isOpen_const] #align is_closed_set_of_cluster_pt isClosed_setOf_clusterPt -theorem mem_closure_iff_clusterPt {s : Set α} {a : α} : a ∈ closure s ↔ ClusterPt a (𝓟 s) := +theorem mem_closure_iff_clusterPt {s : Set X} {a : X} : a ∈ closure s ↔ ClusterPt a (𝓟 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 α} : a ∈ closure s ↔ 𝓝 a ⊓ 𝓟 s ≠ ⊥ := +theorem mem_closure_iff_nhds_neBot {s : Set X} : a ∈ closure s ↔ 𝓝 a ⊓ 𝓟 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 ∈ closure s ↔ NeBot (𝓝[s] x) := +theorem mem_closure_iff_nhdsWithin_neBot {s : Set X} {x : X} : 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 ∉ closure s ↔ 𝓝[s] x = ⊥ := by +lemma not_mem_closure_iff_nhdsWithin_eq_bot {s : Set X} {x : X} : 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 space. -/ -theorem dense_compl_singleton (x : α) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : Set α) := by +theorem dense_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : Set X) := by intro y rcases eq_or_ne y x with (rfl | hne) · rwa [mem_closure_iff_nhdsWithin_neBot] @@ -1346,95 +1345,95 @@ theorem dense_compl_singleton (x : α) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : S /-- If `x` is not an isolated point of a topological space, then the closure of `{x}ᶜ` is the whole space. -/ -- porting note: was a `@[simp]` lemma but `simp` can prove it -theorem closure_compl_singleton (x : α) [NeBot (𝓝[≠] x)] : closure {x}ᶜ = (univ : Set α) := +theorem closure_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : closure {x}ᶜ = (univ : Set X) := (dense_compl_singleton x).closure_eq #align closure_compl_singleton closure_compl_singleton /-- If `x` is not an isolated point of a topological space, then the interior of `{x}` is empty. -/ @[simp] -theorem interior_singleton (x : α) [NeBot (𝓝[≠] x)] : interior {x} = (∅ : Set α) := +theorem interior_singleton (x : X) [NeBot (𝓝[≠] x)] : interior {x} = (∅ : Set X) := interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x) #align interior_singleton interior_singleton -theorem not_isOpen_singleton (x : α) [NeBot (𝓝[≠] x)] : ¬IsOpen ({x} : Set α) := +theorem not_isOpen_singleton (x : X) [NeBot (𝓝[≠] x)] : ¬IsOpen ({x} : Set X) := 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 α} : closure s = { a | ClusterPt a (𝓟 s) } := +theorem closure_eq_cluster_pts {s : Set X} : 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 α} {a : α} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (t ∩ s).Nonempty := +theorem mem_closure_iff_nhds {s : Set X} {a : X} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (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 α} {a : α} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, ∃ y : s, ↑y ∈ t := by +theorem mem_closure_iff_nhds' {s : Set X} {a : X} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, ∃ 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 ∈ closure A ↔ NeBot (comap ((↑) : A → α) (𝓝 x)) := by +theorem mem_closure_iff_comap_neBot {A : Set X} {x : X} : + x ∈ closure A ↔ NeBot (comap ((↑) : A → 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 : α} {p : ι → Prop} {s : ι → Set α} (h : (𝓝 a).HasBasis p s) - {t : Set α} : a ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty := +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 := 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 : α} {p : ι → Prop} {s : ι → Set α} (h : (𝓝 a).HasBasis p s) - {t : Set α} : a ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i := +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 := (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 α} {a : α} : +theorem clusterPt_iff_forall_mem_closure {F : Filter X} {a : X} : ClusterPt a F ↔ ∀ s ∈ F, a ∈ closure s := by simp_rw [ClusterPt, inf_neBot_iff, mem_closure_iff_nhds] rw [forall₂_swap] -theorem clusterPt_iff_lift'_closure {F : Filter α} {a : α} : +theorem clusterPt_iff_lift'_closure {F : Filter X} {a : X} : ClusterPt a F ↔ pure a ≤ (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 α} {a : α} : +theorem clusterPt_iff_lift'_closure' {F : Filter X} {a : X} : ClusterPt a F ↔ (F.lift' closure ⊓ pure a).NeBot := by rw [clusterPt_iff_lift'_closure, ← Ultrafilter.coe_pure, inf_comm, Ultrafilter.inf_neBot_iff] @[simp] -theorem clusterPt_lift'_closure_iff {F : Filter α} {a : α} : +theorem clusterPt_lift'_closure_iff {F : Filter X} {a : X} : ClusterPt a (F.lift' closure) ↔ ClusterPt a F := by - simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure α) (monotone_closure α)] + 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 ∈ closure s ↔ ∃ u : Ultrafilter α, s ∈ u ∧ ↑u ≤ 𝓝 x := by +theorem mem_closure_iff_ultrafilter {s : Set X} {x : X} : + 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 α} : IsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s := +theorem isClosed_iff_clusterPt {s : Set X} : 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 α} : +theorem isClosed_iff_nhds {s : Set X} : 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 α} : - IsClosed s ↔ ∀ x, ∀ F : Filter α, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s := by +lemma isClosed_iff_forall_filter {s : Set X} : + 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 α} (_ : IsClosed s) : +theorem IsClosed.interior_union_left {s t : Set X} (_ : 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 @@ -1442,28 +1441,28 @@ theorem IsClosed.interior_union_left {s t : Set α} (_ : IsClosed s) : ⟨ha, h⟩⟩ #align is_closed.interior_union_left IsClosed.interior_union_left -theorem IsClosed.interior_union_right {s t : Set α} (h : IsClosed t) : +theorem IsClosed.interior_union_right {s t : Set X} (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 α} (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t) := +theorem IsOpen.inter_closure {s t : Set X} (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 α} (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t) := by +theorem IsOpen.closure_inter {s t : Set X} (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 α} (hs : Dense s) (ht : IsOpen t) : +theorem Dense.open_subset_closure_inter {s t : Set X} (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 : α} (h : x ∈ closure (s₁ ∪ s₂)) +theorem mem_closure_of_mem_closure_union {s₁ s₂ : Set X} {x : X} (h : x ∈ closure (s₁ ∪ s₂)) (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ := by rw [mem_closure_iff_nhds_neBot] at * rwa [← @@ -1476,24 +1475,24 @@ theorem mem_closure_of_mem_closure_union {s₁ s₂ : Set α} {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 α} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : +theorem Dense.inter_of_isOpen_left {s t : Set X} (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 α} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : +theorem Dense.inter_of_isOpen_right {s t : Set X} (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 α} (hs : Dense s) {x : α} (ht : t ∈ 𝓝 x) : +theorem Dense.inter_nhds_nonempty {s t : Set X} (hs : Dense s) {x : X} (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 α} : closure s \ closure t ⊆ closure (s \ t) := +theorem closure_diff {s t : Set X} : 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 @@ -1501,35 +1500,35 @@ theorem closure_diff {s t : Set α} : 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 : α} {s : Set α} (h : ∃ᶠ x in 𝓝 a, x ∈ s) +theorem Filter.Frequently.mem_of_closed {a : X} {s : Set X} (h : ∃ᶠ x in 𝓝 a, x ∈ s) (hs : IsClosed s) : a ∈ 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 : β → α} {b : Filter β} {a : α} {s : Set α} +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 := (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 : β → α} {b : Filter β} {a : α} {s : Set α} [NeBot b] +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 := 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 : β → α} {b : Filter β} {a : α} {s : Set α} +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 := (hf.frequently h).mem_closure #align mem_closure_of_frequently_of_tendsto mem_closure_of_frequently_of_tendsto -theorem mem_closure_of_tendsto {f : β → α} {b : Filter β} {a : α} {s : Set α} [NeBot b] +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 := 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 : β → α} {l : Filter β} {s : Set β} {a : α} - (h : ∀ (x) (_ : x ∉ s), f x = a) : Tendsto f (l ⊓ 𝓟 s) (𝓝 a) ↔ Tendsto f l (𝓝 a) := by +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 rw [tendsto_iff_comap, tendsto_iff_comap] replace h : 𝓟 sᶜ ≤ comap f (𝓝 a) · rintro U ⟨t, ht, htU⟩ x hx @@ -1558,37 +1557,37 @@ section lim 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 α] (f : Filter α) : α := +noncomputable def lim [Nonempty X] (f : Filter X) : X := Classical.epsilon fun a => f ≤ 𝓝 a #align Lim lim /-- If `F` is an ultrafilter, then `Filter.Ultrafilter.lim F` is a limit of the filter, if it exists. -Note that dot notation `F.lim` can be used for `F : Filter.Ultrafilter α`. +Note that dot notation `F.lim` can be used for `F : Filter.Ultrafilter X`. -/ -noncomputable nonrec def Ultrafilter.lim (F : Ultrafilter α) : α := - @lim α _ (nonempty_of_neBot F) F +noncomputable nonrec def Ultrafilter.lim (F : Ultrafilter X) : X := + @lim X _ (nonempty_of_neBot F) F #align ultrafilter.Lim Ultrafilter.lim -/-- If `f` is a filter in `β` and `g : β → α` is a function, then `limUnder f g` is a limit of `g` +/-- If `f` is a filter in `α` and `g : α → X` is a function, then `limUnder f g` is a limit of `g` at `f`, if it exists. -/ -noncomputable def limUnder [Nonempty α] (f : Filter β) (g : β → α) : α := +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 -formulate this lemma with a `[Nonempty α]` argument of `lim` derived from `h` to make it useful for -types without a `[Nonempty α]` instance. Because of the built-in proof irrelevance, Lean will unify +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 α} (h : ∃ a, f ≤ 𝓝 a) : f ≤ 𝓝 (@lim _ _ (nonempty_of_exists h) f) := +theorem le_nhds_lim {f : Filter X} (h : ∃ a, f ≤ 𝓝 a) : 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 -this lemma with a `[Nonempty α]` argument of `lim` derived from `h` to make it useful for types -without a `[Nonempty α]` instance. Because of the built-in proof irrelevance, Lean will unify this +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 : β → α} (h : ∃ a, Tendsto g f (𝓝 a)) : +theorem tendsto_nhds_limUnder {f : Filter α} {g : α → X} (h : ∃ a, Tendsto g f (𝓝 a)) : Tendsto g f (𝓝 (@limUnder _ _ _ (nonempty_of_exists h) f g)) := le_nhds_lim h #align tendsto_nhds_lim tendsto_nhds_limUnder @@ -1605,15 +1604,13 @@ open Topology section Continuous -variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} - -variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] +variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] open TopologicalSpace /-- A function between topological spaces is continuous if the preimage of every open set is open. Registered as a structure to make sure it is not unfolded by Lean. -/ -structure Continuous (f : α → β) : Prop where +structure Continuous (f : X → Y) : Prop where /-- The preimage of an open set under a continuous function is an open set. Use `IsOpen.preimage` instead. -/ isOpen_preimage : ∀ s, IsOpen s → IsOpen (f ⁻¹' s) @@ -1624,227 +1621,227 @@ set_option quotPrecheck false in scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" => @Continuous _ _ t₁ t₂ -theorem continuous_def {_ : TopologicalSpace α} {_ : TopologicalSpace β} {f : α → β} : +theorem continuous_def {_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) := ⟨fun hf => hf.1, fun h => ⟨h⟩⟩ #align continuous_def continuous_def -theorem IsOpen.preimage {f : α → β} (hf : Continuous f) {s : Set β} (h : IsOpen s) : +theorem IsOpen.preimage {f : X → Y} (hf : Continuous f) {s : Set Y} (h : IsOpen s) : IsOpen (f ⁻¹' s) := hf.isOpen_preimage s h #align is_open.preimage IsOpen.preimage -theorem continuous_congr {f g : α → β} (h : ∀ x, f x = g x) : +theorem continuous_congr {f g : X → Y} (h : ∀ x, f x = g x) : Continuous f ↔ Continuous g := .of_eq <| congrArg _ <| funext h -theorem Continuous.congr {f g : α → β} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g := +theorem Continuous.congr {f g : X → Y} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g := continuous_congr h' |>.mp h #align continuous.congr Continuous.congr /-- A function between topological spaces is continuous at a point `x₀` if `f x` tends to `f x₀` when `x` tends to `x₀`. -/ -def ContinuousAt (f : α → β) (x : α) := +def ContinuousAt (f : X → Y) (x : X) := Tendsto f (𝓝 x) (𝓝 (f x)) #align continuous_at ContinuousAt -theorem ContinuousAt.tendsto {f : α → β} {x : α} (h : ContinuousAt f x) : +theorem ContinuousAt.tendsto {f : X → Y} {x : X} (h : ContinuousAt f x) : Tendsto f (𝓝 x) (𝓝 (f x)) := h #align continuous_at.tendsto ContinuousAt.tendsto -theorem continuousAt_def {f : α → β} {x : α} : ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x := +theorem continuousAt_def {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x := Iff.rfl #align continuous_at_def continuousAt_def -theorem continuousAt_congr {f g : α → β} {x : α} (h : f =ᶠ[𝓝 x] g) : +theorem continuousAt_congr {f g : X → Y} {x : X} (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 : α} (hf : ContinuousAt f x) (h : f =ᶠ[𝓝 x] g) : +theorem ContinuousAt.congr {f g : X → Y} {x : X} (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 : α} {t : Set β} (h : ContinuousAt f x) +theorem ContinuousAt.preimage_mem_nhds {f : X → Y} {x : X} {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 : α} {f : α → M₀} : +theorem eventuallyEq_zero_nhds {M₀} [Zero M₀] {a : X} {f : X → M₀} : f =ᶠ[𝓝 a] 0 ↔ a ∉ 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 : α} {la : Filter α} {lb : Filter β} (H : ClusterPt x la) {f : α → β} +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 := (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 : α → β} {s : Set β} (hf : Continuous f) : +theorem preimage_interior_subset_interior_preimage {f : X → Y} {s : Set Y} (hf : Continuous f) : f ⁻¹' interior s ⊆ interior (f ⁻¹' s) := interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf) #align preimage_interior_subset_interior_preimage preimage_interior_subset_interior_preimage @[continuity] -theorem continuous_id : Continuous (id : α → α) := +theorem continuous_id : Continuous (id : X → X) := continuous_def.2 fun _ => id #align continuous_id continuous_id -- This is needed due to reducibility issues with the `continuity` tactic. @[continuity] -theorem continuous_id' : Continuous (fun (x : α) => x) := continuous_id +theorem continuous_id' : Continuous (fun (x : X) => x) := continuous_id -theorem Continuous.comp {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) : +theorem Continuous.comp {g : Y → Z} {f : X → Y} (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 : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) : +theorem Continuous.comp' {g : Y → Z} {f : X → Y} (hg : Continuous g) (hf : Continuous f) : Continuous (fun x => g (f x)) := hg.comp hf -theorem Continuous.iterate {f : α → α} (h : Continuous f) (n : ℕ) : Continuous f^[n] := +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 : β → γ} {f : α → β} {x : α} (hg : ContinuousAt g (f x)) +nonrec theorem ContinuousAt.comp {g : Y → Z} {f : X → Y} {x : X} (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 : β → γ} {f : α → β} {x : α} {y : β} (hg : ContinuousAt g y) +theorem ContinuousAt.comp_of_eq {g : Y → Z} {f : X → Y} {x : X} {y : Y} (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 : α → β} (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) := +theorem Continuous.tendsto {f : X → Y} (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 : α → β} (hf : Continuous f) (x : α) (y : β) (h : f x = y) : +theorem Continuous.tendsto' {f : X → Y} (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 : α} (h : Continuous f) : ContinuousAt f x := +theorem Continuous.continuousAt {f : X → Y} {x : X} (h : Continuous f) : ContinuousAt f x := h.tendsto x #align continuous.continuous_at Continuous.continuousAt -theorem continuous_iff_continuousAt {f : α → β} : Continuous f ↔ ∀ x, ContinuousAt f x := +theorem continuous_iff_continuousAt {f : X → Y} : 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 : α} {b : β} : ContinuousAt (fun _ : α => b) x := +theorem continuousAt_const {x : X} {b : Y} : ContinuousAt (fun _ : X => b) x := tendsto_const_nhds #align continuous_at_const continuousAt_const @[continuity] -theorem continuous_const {b : β} : Continuous fun _ : α => b := +theorem continuous_const {b : Y} : Continuous fun _ : X => b := continuous_iff_continuousAt.mpr fun _ => continuousAt_const #align continuous_const continuous_const -theorem Filter.EventuallyEq.continuousAt {x : α} {f : α → β} {y : β} (h : f =ᶠ[𝓝 x] fun _ => y) : +theorem Filter.EventuallyEq.continuousAt {x : X} {f : X → Y} {y : Y} (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 : α → β} (h : ∀ x y, f x = f y) : Continuous f := +theorem continuous_of_const {f : X → Y} (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 : α} : ContinuousAt id x := +theorem continuousAt_id {x : X} : ContinuousAt id x := continuous_id.continuousAt #align continuous_at_id continuousAt_id -theorem ContinuousAt.iterate {f : α → α} {x : α} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) : +theorem ContinuousAt.iterate {f : X → X} {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 : α → β} : Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) := +theorem continuous_iff_isClosed {f : X → Y} : 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 : α → β} (hf : Continuous f) {s : Set β} (h : IsClosed s) : +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 #align is_closed.preimage IsClosed.preimage -theorem mem_closure_image {f : α → β} {x : α} {s : Set α} (hf : ContinuousAt f x) +theorem mem_closure_image {f : X → Y} {x : X} {s : Set X} (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} : - ContinuousAt f x ↔ ∀ g : Ultrafilter α, ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) := +theorem continuousAt_iff_ultrafilter {f : X → Y} {x} : + 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 : α → β} : - Continuous f ↔ ∀ (x) (g : Ultrafilter α), ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) := by +theorem continuous_iff_ultrafilter {f : X → Y} : + 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 : α → β} (hf : Continuous f) (t : Set β) : +theorem Continuous.closure_preimage_subset {f : X → Y} (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 : α → β} (hf : Continuous f) (t : Set β) : +theorem Continuous.frontier_preimage_subset {f : X → Y} (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 α} {t : Set β} {f : α → β} (h : MapsTo f s t) +protected theorem Set.MapsTo.closure {s : Set X} {t : Set Y} {f : X → 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 : α → β} {s : Set α} (h : Continuous f) : +theorem image_closure_subset_closure_image {f : X → Y} {s : Set X} (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 : α → β} {s : Set α} (h : Continuous f) : +theorem closure_image_closure {f : X → Y} {s : Set X} (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 : α → β} {s : Set α} (h : Continuous f) : +theorem closure_subset_preimage_closure_image {f : X → Y} {s : Set X} (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 α} {t : Set β} {f : α → β} {a : α} (hf : Continuous f) +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 #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 α} {t : Set β} {f : α → β} (h : MapsTo f s t) +theorem Set.MapsTo.closure_left {s : Set X} {t : Set Y} {f : X → 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 @@ -1855,9 +1852,9 @@ theorem Set.MapsTo.closure_left {s : Set α} {t : Set β} {f : α → β} (h : M section DenseRange -variable {κ ι : Type*} (f : κ → β) (g : β → γ) +variable {α ι : Type*} (f : α → X) (g : X → Y) -/-- `f : ι → β` has dense range if its range (image) is a dense subset of β. -/ +/-- `f : α → X` has dense range if its range (image) is a dense subset of `X`. -/ def DenseRange := Dense (range f) #align dense_range DenseRange @@ -1868,7 +1865,7 @@ theorem Function.Surjective.denseRange (hf : Function.Surjective f) : DenseRange simp [hf.range_eq] #align function.surjective.dense_range Function.Surjective.denseRange -theorem denseRange_id : DenseRange (id : α → α) := +theorem denseRange_id : DenseRange (id : X → X) := Function.Surjective.denseRange Function.surjective_id #align dense_range_id denseRange_id @@ -1880,25 +1877,25 @@ 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 α} (h : Dense s) : DenseRange ((↑) : s → α) := by +theorem Dense.denseRange_val {s : Set X} (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 : α → β} (hf : Continuous f) {s : Set α} +theorem Continuous.range_subset_closure_image_dense {f : X → Y} (hf : Continuous f) {s : Set X} (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 : α → β} (hf' : DenseRange f) (hf : Continuous f) {s : Set α} +theorem DenseRange.dense_image {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) {s : Set X} (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 β} +theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) {s : Set X} (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s)) := by rw [image_preimage_eq_inter_range] exact hf.open_subset_closure_inter hs @@ -1906,38 +1903,38 @@ theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) { /-- 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 : α → β} (hf' : DenseRange f) (hf : Continuous f) {s : Set α} - (hs : Dense s) {t : Set β} (ht : MapsTo f s t) : Dense t := +theorem DenseRange.dense_of_mapsTo {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) {s : Set X} + (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 /-- Composition of a continuous map with dense range and a function with dense range has dense range. -/ -theorem DenseRange.comp {g : β → γ} {f : κ → β} (hg : DenseRange g) (hf : DenseRange f) +theorem DenseRange.comp {g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f) (cg : Continuous g) : DenseRange (g ∘ f) := by rw [DenseRange, range_comp] exact hg.dense_image cg hf #align dense_range.comp DenseRange.comp -nonrec theorem DenseRange.nonempty_iff (hf : DenseRange f) : Nonempty κ ↔ Nonempty β := +nonrec theorem DenseRange.nonempty_iff (hf : DenseRange f) : Nonempty α ↔ Nonempty X := range_nonempty_iff_nonempty.symm.trans hf.nonempty_iff #align dense_range.nonempty_iff DenseRange.nonempty_iff -theorem DenseRange.nonempty [h : Nonempty β] (hf : DenseRange f) : Nonempty κ := +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 : α → β` with dense range and `b : β`, returns some `a : α`. -/ -def DenseRange.some (hf : DenseRange f) (b : β) : κ := +/-- 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⟩ #align dense_range.some DenseRange.some -nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) {s : Set β} (ho : IsOpen s) +nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) {s : Set X} (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 {f : κ → β} (h : DenseRange f) {b : β} {U : Set β} (U_in : U ∈ 𝓝 b) : +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⟩ ⟨a, interior_subset ha⟩ @@ -1991,7 +1988,7 @@ This has the following advantages As an example for a unary operation, we have `Continuous.neg`. ``` -Continuous.neg {f : α → G} (hf : Continuous f) : Continuous (fun x ↦ -f x) +Continuous.neg {f : X → G} (hf : Continuous f) : Continuous (fun x ↦ -f x) ``` For unary functions, the elaborator is not confused when applying the traditional lemma (like `continuous_neg`), but it's still convenient to have the short version available (compare @@ -2063,7 +2060,7 @@ Only after elaborating the two `ContinuousAt` arguments, Lean will try to unify which is often easy after having chosen the correct functions for `f` and `g`. Here is an example that shows the difference: ``` -example [TopologicalSpace α] [TopologicalSpace β] {x₀ : α} (f : α → α → β) +example [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} (f : X → X → Y) (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) : ContinuousAt (fun x ↦ f x x) x₀ := -- hf.comp (continuousAt_id.prod continuousAt_id) -- type mismatch diff --git a/Mathlib/Topology/MetricSpace/Polish.lean b/Mathlib/Topology/MetricSpace/Polish.lean index a4df6bfea158c..232d2b160fe09 100644 --- a/Mathlib/Topology/MetricSpace/Polish.lean +++ b/Mathlib/Topology/MetricSpace/Polish.lean @@ -406,8 +406,7 @@ theorem _root_.IsClosed.isClopenable [TopologicalSpace α] [PolishSpace α] {s : · rw [← f.induced_symm] exact f.symm.polishSpace_induced · rw [isOpen_coinduced, isOpen_sum_iff] - convert And.intro (isOpen_univ (α := s)) (isOpen_empty (α := (sᶜ : Set α))) - <;> ext ⟨x, hx⟩ <;> simpa using hx + simp [preimage_preimage] #align is_closed.is_clopenable IsClosed.isClopenable theorem IsClopenable.compl [TopologicalSpace α] {s : Set α} (hs : IsClopenable s) :