topology.partial

# Partial functions and topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : filter β} {a : α} :
(nhds a) (s : set α), a s r.core s l
theorem rtendsto'_nhds {α : Type u_1} {β : Type u_2} {r : rel β α} {l : filter β} {a : α} :
(nhds a) (s : set α), a s r.preimage s l
theorem ptendsto_nhds {α : Type u_1} {β : Type u_2} {f : β →. α} {l : filter β} {a : α} :
(nhds a) (s : set α), a s f.core s l
theorem ptendsto'_nhds {α : Type u_1} {β : Type u_2} {f : β →. α} {l : filter β} {a : α} :
(nhds a) (s : set α), a s f.preimage s l

### Continuity and partial functions #

def pcontinuous {α : Type u_1} {β : Type u_2} (f : α →. β) :
Prop

Continuity of a partial function

Equations
theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} {f : α →. β} (h : pcontinuous f) :
theorem pcontinuous_iff' {α : Type u_1} {β : Type u_2} {f : α →. β} :
{x : α} {y : β}, y f x (nhds x) (nhds y)
theorem continuous_within_at_iff_ptendsto_res {α : Type u_1} {β : Type u_2} (f : α β) {x : α} {s : set α} :
x filter.ptendsto (pfun.res f s) (nhds x) (nhds (f x))