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

Continuity and partial functions #

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

Continuity of a partial function

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