Partial functions and topological spaces

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.

theorem rtendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {r : Rel Y X} {l : Filter Y} {x : X} : Filter.RTendsto r l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → Rel.core r s ∈ l

theorem rtendsto'_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {r : Rel Y X} {l : Filter Y} {x : X} : Filter.RTendsto' r l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → Rel.preimage r s ∈ l

theorem ptendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : Y →. X} {l : Filter Y} {x : X} : Filter.PTendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → PFun.core f s ∈ l

theorem ptendsto'_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : Y →. X} {l : Filter Y} {x : X} : Filter.PTendsto' f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → PFun.preimage f s ∈ l

Continuity and partial functions

def PContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X →. Y) : Prop

Continuity of a partial function

Equations

• PContinuous f = ∀ (s : Set Y), IsOpen s → IsOpen (PFun.preimage f s)

theorem open_dom_of_pcontinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X →. Y} (h : PContinuous f) : IsOpen (PFun.Dom f)

theorem pcontinuous_iff' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X →. Y} : PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → Filter.PTendsto' f (nhds x) (nhds y)

theorem continuousWithinAt_iff_ptendsto_res {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) {x : X} {s : Set X} : ContinuousWithinAt f s x ↔ Filter.PTendsto (PFun.res f s) (nhds x) (nhds (f x))