mathlib3 documentation

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

Continuity and partial functions #

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

Continuity of a partial function

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