style: rename Rtendsto and Ptendsto to RTendsto and PTendsto (#…

…4722)

#2203

Mathlib/Order/Filter/Partial.lean

@@ -88,15 +88,15 @@ theorem rmap_compose (r : Rel α β) (s : Rel β γ) : rmap s ∘ rmap r = rmap
   funext <| rmap_rmap _ _
 #align filter.rmap_compose Filter.rmap_compose
 
-/-- Generic "limit of a relation" predicate. `Rtendsto r l₁ l₂` asserts that for every
+/-- Generic "limit of a relation" predicate. `RTendsto r l₁ l₂` asserts that for every
 `l₂`-neighborhood `a`, the `r`-core of `a` is an `l₁`-neighborhood. One generalization of
 `Filter.Tendsto` to relations. -/
-def Rtendsto (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :=
+def RTendsto (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :=
   l₁.rmap r ≤ l₂
-#align filter.rtendsto Filter.Rtendsto
+#align filter.rtendsto Filter.RTendsto
 
 theorem rtendsto_def (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
-    Rtendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁ :=
+    RTendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁ :=
   Iff.rfl
 #align filter.rtendsto_def Filter.rtendsto_def
 
@@ -131,7 +131,7 @@ theorem rcomap_compose (r : Rel α β) (s : Rel β γ) : rcomap r ∘ rcomap s =
 #align filter.rcomap_compose Filter.rcomap_compose
 
 theorem rtendsto_iff_le_rcomap (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
-    Rtendsto r l₁ l₂ ↔ l₁ ≤ l₂.rcomap r := by
+    RTendsto r l₁ l₂ ↔ l₁ ≤ l₂.rcomap r := by
   rw [rtendsto_def]
   simp_rw [←l₂.mem_sets]
   simp [Filter.le_def, rcomap, Rel.mem_image]; constructor
@@ -181,27 +181,27 @@ theorem rcomap'_compose (r : Rel α β) (s : Rel β γ) : rcomap' r ∘ rcomap'
   funext <| rcomap'_rcomap' _ _
 #align filter.rcomap'_compose Filter.rcomap'_compose
 
-/-- Generic "limit of a relation" predicate. `Rtendsto' r l₁ l₂` asserts that for every
+/-- Generic "limit of a relation" predicate. `RTendsto' r l₁ l₂` asserts that for every
 `l₂`-neighborhood `a`, the `r`-preimage of `a` is an `l₁`-neighborhood. One generalization of
 `Filter.Tendsto` to relations. -/
-def Rtendsto' (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :=
+def RTendsto' (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :=
   l₁ ≤ l₂.rcomap' r
-#align filter.rtendsto' Filter.Rtendsto'
+#align filter.rtendsto' Filter.RTendsto'
 
 theorem rtendsto'_def (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
-    Rtendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁ := by
-  unfold Rtendsto' rcomap'; simp [le_def, Rel.mem_image]; constructor
+    RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁ := by
+  unfold RTendsto' rcomap'; simp [le_def, Rel.mem_image]; constructor
   · exact fun h s hs => h _ _ hs Set.Subset.rfl
   · exact fun h s t ht => mem_of_superset (h t ht)
 #align filter.rtendsto'_def Filter.rtendsto'_def
 
 theorem tendsto_iff_rtendsto (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
-    Tendsto f l₁ l₂ ↔ Rtendsto (Function.graph f) l₁ l₂ := by
+    Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂ := by
   simp [tendsto_def, Function.graph, rtendsto_def, Rel.core, Set.preimage]
 #align filter.tendsto_iff_rtendsto Filter.tendsto_iff_rtendsto
 
 theorem tendsto_iff_rtendsto' (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
-    Tendsto f l₁ l₂ ↔ Rtendsto' (Function.graph f) l₁ l₂ := by
+    Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂ := by
   simp [tendsto_def, Function.graph, rtendsto'_def, Rel.preimage_def, Set.preimage]
 #align filter.tendsto_iff_rtendsto' Filter.tendsto_iff_rtendsto'
 
@@ -219,20 +219,20 @@ theorem mem_pmap (f : α →. β) (l : Filter α) (s : Set β) : s ∈ l.pmap f
   Iff.rfl
 #align filter.mem_pmap Filter.mem_pmap
 
-/-- Generic "limit of a partial function" predicate. `Ptendsto r l₁ l₂` asserts that for every
+/-- Generic "limit of a partial function" predicate. `PTendsto r l₁ l₂` asserts that for every
 `l₂`-neighborhood `a`, the `p`-core of `a` is an `l₁`-neighborhood. One generalization of
 `Filter.Tendsto` to partial function. -/
-def Ptendsto (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :=
+def PTendsto (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :=
   l₁.pmap f ≤ l₂
-#align filter.ptendsto Filter.Ptendsto
+#align filter.ptendsto Filter.PTendsto
 
 theorem ptendsto_def (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :
-    Ptendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f.core s ∈ l₁ :=
+    PTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f.core s ∈ l₁ :=
   Iff.rfl
 #align filter.ptendsto_def Filter.ptendsto_def
 
 theorem ptendsto_iff_rtendsto (l₁ : Filter α) (l₂ : Filter β) (f : α →. β) :
-    Ptendsto f l₁ l₂ ↔ Rtendsto f.graph' l₁ l₂ :=
+    PTendsto f l₁ l₂ ↔ RTendsto f.graph' l₁ l₂ :=
   Iff.rfl
 #align filter.ptendsto_iff_rtendsto Filter.ptendsto_iff_rtendsto
 
@@ -244,12 +244,12 @@ theorem pmap_res (l : Filter α) (s : Set α) (f : α → β) :
 #align filter.pmap_res Filter.pmap_res
 
 theorem tendsto_iff_ptendsto (l₁ : Filter α) (l₂ : Filter β) (s : Set α) (f : α → β) :
-    Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ Ptendsto (PFun.res f s) l₁ l₂ := by
-  simp only [Tendsto, Ptendsto, pmap_res]
+    Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂ := by
+  simp only [Tendsto, PTendsto, pmap_res]
 #align filter.tendsto_iff_ptendsto Filter.tendsto_iff_ptendsto
 
 theorem tendsto_iff_ptendsto_univ (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
-    Tendsto f l₁ l₂ ↔ Ptendsto (PFun.res f Set.univ) l₁ l₂ := by
+    Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂ := by
   rw [← tendsto_iff_ptendsto]
   simp [principal_univ]
 #align filter.tendsto_iff_ptendsto_univ Filter.tendsto_iff_ptendsto_univ
@@ -260,26 +260,26 @@ def pcomap' (f : α →. β) (l : Filter β) : Filter α :=
   Filter.rcomap' f.graph' l
 #align filter.pcomap' Filter.pcomap'
 
-/-- Generic "limit of a partial function" predicate. `Ptendsto' r l₁ l₂` asserts that for every
+/-- Generic "limit of a partial function" predicate. `PTendsto' r l₁ l₂` asserts that for every
 `l₂`-neighborhood `a`, the `p`-preimage of `a` is an `l₁`-neighborhood. One generalization of
 `Filter.Tendsto` to partial functions. -/
-def Ptendsto' (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :=
+def PTendsto' (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :=
   l₁ ≤ l₂.rcomap' f.graph'
-#align filter.ptendsto' Filter.Ptendsto'
+#align filter.ptendsto' Filter.PTendsto'
 
 theorem ptendsto'_def (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :
-    Ptendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁ :=
+    PTendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁ :=
   rtendsto'_def _ _ _
 #align filter.ptendsto'_def Filter.ptendsto'_def
 
 theorem ptendsto_of_ptendsto' {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} :
-    Ptendsto' f l₁ l₂ → Ptendsto f l₁ l₂ := by
+    PTendsto' f l₁ l₂ → PTendsto f l₁ l₂ := by
   rw [ptendsto_def, ptendsto'_def]
   exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)
 #align filter.ptendsto_of_ptendsto' Filter.ptendsto_of_ptendsto'
 
 theorem ptendsto'_of_ptendsto {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} (h : f.Dom ∈ l₁) :
-    Ptendsto f l₁ l₂ → Ptendsto' f l₁ l₂ := by
+    PTendsto f l₁ l₂ → PTendsto' f l₁ l₂ := by
   rw [ptendsto_def, ptendsto'_def]
   intro h' s sl₂
   rw [PFun.preimage_eq]

Mathlib/Topology/Partial.lean

@@ -14,7 +14,7 @@ import Mathlib.Order.Filter.Partial
 /-!
 # Partial functions and topological spaces
 
-In this file we prove properties of `Filter.Ptendsto` etc in topological spaces. We also introduce
+In this file we prove properties of `Filter.PTendsto` etc in topological spaces. We also introduce
 `PContinuous`, a version of `Continuous` for partially defined functions.
 -/
 
@@ -26,24 +26,24 @@ open Topology
 variable {α β : Type _} [TopologicalSpace α]
 
 theorem rtendsto_nhds {r : Rel β α} {l : Filter β} {a : α} :
-    Rtendsto r l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → r.core s ∈ l :=
+    RTendsto r l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → r.core s ∈ l :=
   all_mem_nhds_filter _ _ (fun _s _t => id) _
 #align rtendsto_nhds rtendsto_nhds
 
 theorem rtendsto'_nhds {r : Rel β α} {l : Filter β} {a : α} :
-    Rtendsto' r l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → r.preimage s ∈ l := by
+    RTendsto' r l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → r.preimage s ∈ l := by
   rw [rtendsto'_def]
   apply all_mem_nhds_filter
   apply Rel.preimage_mono
 #align rtendsto'_nhds rtendsto'_nhds
 
 theorem ptendsto_nhds {f : β →. α} {l : Filter β} {a : α} :
-    Ptendsto f l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → f.core s ∈ l :=
+    PTendsto f l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → f.core s ∈ l :=
   rtendsto_nhds
 #align ptendsto_nhds ptendsto_nhds
 
 theorem ptendsto'_nhds {f : β →. α} {l : Filter β} {a : α} :
-    Ptendsto' f l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → f.preimage s ∈ l :=
+    PTendsto' f l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → f.preimage s ∈ l :=
   rtendsto'_nhds
 #align ptendsto'_nhds ptendsto'_nhds
 
@@ -62,7 +62,7 @@ theorem open_dom_of_pcontinuous {f : α →. β} (h : PContinuous f) : IsOpen f.
 #align open_dom_of_pcontinuous open_dom_of_pcontinuous
 
 theorem pcontinuous_iff' {f : α →. β} :
-    PContinuous f ↔ ∀ {x y} (h : y ∈ f x), Ptendsto' f (𝓝 x) (𝓝 y) := by
+    PContinuous f ↔ ∀ {x y} (h : y ∈ f x), PTendsto' f (𝓝 x) (𝓝 y) := by
   constructor
   · intro h x y h'
     simp only [ptendsto'_def, mem_nhds_iff]
@@ -77,7 +77,7 @@ theorem pcontinuous_iff' {f : α →. β} :
   apply mem_of_superset _ h
   have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x := by
     intro s hs
-    have : Ptendsto' f (𝓝 x) (𝓝 y) := hf fxy
+    have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
     rw [ptendsto'_def] at this
     exact this s hs
   show f.preimage s ∈ 𝓝 x
@@ -87,6 +87,6 @@ theorem pcontinuous_iff' {f : α →. β} :
 #align pcontinuous_iff' pcontinuous_iff'
 
 theorem continuousWithinAt_iff_ptendsto_res (f : α → β) {x : α} {s : Set α} :
-    ContinuousWithinAt f s x ↔ Ptendsto (PFun.res f s) (𝓝 x) (𝓝 (f x)) :=
+    ContinuousWithinAt f s x ↔ PTendsto (PFun.res f s) (𝓝 x) (𝓝 (f x)) :=
   tendsto_iff_ptendsto _ _ _ _
 #align continuous_within_at_iff_ptendsto_res continuousWithinAt_iff_ptendsto_res