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 : α}
:
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 : α}
:
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 : α →. β)
:
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 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))