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 s → a ∈ s → Rel.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 s → a ∈ s → Rel.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 s → a ∈ s → PFun.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 s → a ∈ s → PFun.preimage f s ∈ l

Continuity and partial functions

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

Continuity of a partial function

theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α →. β} (h : PContinuous f) : IsOpen (PFun.Dom f)

theorem pcontinuous_iff' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α →. β} : PContinuous f ↔ ∀ {x : α} {y : β}, y ∈ f x → Filter.PTendsto' f (nhds x) (nhds y)

theorem continuousWithinAt_iff_ptendsto_res {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {x : α} {s : Set α} : ContinuousWithinAt f s x ↔ Filter.PTendsto (PFun.res f s) (nhds x) (nhds (f x))