# 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} [] {r : Rel Y X} {l : } {x : X} :
Filter.RTendsto r l (nhds x) ∀ (s : Set X), x sr.core s l
theorem rtendsto'_nhds {X : Type u_1} {Y : Type u_2} [] {r : Rel Y X} {l : } {x : X} :
Filter.RTendsto' r l (nhds x) ∀ (s : Set X), x sr.preimage s l
theorem ptendsto_nhds {X : Type u_1} {Y : Type u_2} [] {f : Y →. X} {l : } {x : X} :
Filter.PTendsto f l (nhds x) ∀ (s : Set X), x sf.core s l
theorem ptendsto'_nhds {X : Type u_1} {Y : Type u_2} [] {f : Y →. X} {l : } {x : X} :
Filter.PTendsto' f l (nhds x) ∀ (s : Set X), x sf.preimage s l

### Continuity and partial functions #

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

Continuity of a partial function

Equations
Instances For
theorem open_dom_of_pcontinuous {X : Type u_1} {Y : Type u_2} [] [] {f : X →. Y} (h : ) :
IsOpen f.Dom
theorem pcontinuous_iff' {X : Type u_1} {Y : Type u_2} [] [] {f : X →. Y} :
∀ {x : X} {y : Y}, y f xFilter.PTendsto' f (nhds x) (nhds y)
theorem continuousWithinAt_iff_ptendsto_res {X : Type u_1} {Y : Type u_2} [] [] (f : XY) {x : X} {s : Set X} :
Filter.PTendsto (PFun.res f s) (nhds x) (nhds (f x))