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.

source

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

source

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

source

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

source

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 #

source

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

Prop

Continuity of a partial function

Equations

pcontinuous f = ∀ (s : set β), is_open s → is_open (f.preimage s)

source

theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} (h : pcontinuous f) :

is_open f.dom

source

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)

source

theorem continuous_within_at_iff_ptendsto_res {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) {x : α} {s : set α} :

continuous_within_at f s x ↔ filter.ptendsto (pfun.res f s) (nhds x) (nhds (f x))