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 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {r : Rel Y X} {l : Filter Y} {x : X} :
Filter.RTendsto r l (nhds x) ∀ (s : Set X), IsOpen sx sr.core s l
theorem rtendsto'_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {r : Rel Y X} {l : Filter Y} {x : X} :
Filter.RTendsto' r l (nhds x) ∀ (s : Set X), IsOpen sx sr.preimage s l
theorem ptendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : Y →. X} {l : Filter Y} {x : X} :
Filter.PTendsto f l (nhds x) ∀ (s : Set X), IsOpen sx sf.core s l
theorem ptendsto'_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : Y →. X} {l : Filter Y} {x : X} :
Filter.PTendsto' f l (nhds x) ∀ (s : Set X), IsOpen sx sf.preimage s l

Continuity and partial functions #

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

Continuity of a partial function

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