# Documentation

Mathlib.Topology.Partial

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

### Continuity and partial functions #

def PContinuous {α : Type u_1} {β : Type u_2} [] [] (f : α →. β) :

Continuity of a partial function

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