Neighborhoods and continuity relative to a subset #
This file defines relative versions
and proves their basic properties, including the relationships between these restricted notions and the corresponding notions for the subtype equipped with the subspace topology.
Notation #
𝓝 x
: the filter of neighborhoods of a pointx
;𝓟 s
: the principal filter of a sets
;𝓝[s] x
: the filternhdsWithin x s
of neighborhoods of a pointx
within a sets
.
Alias of eventually_eventually_nhdsWithin
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
nhdsWithin
and subtypes #
If a function is continuous within s
at x
, then it tends to f x
within s
by definition.
We register this fact for use with the dot notation, especially to use Filter.Tendsto.comp
as
ContinuousWithinAt.comp
will have a different meaning.
If a function f a b
is such that y ↦ f a b
is continuous for all a
, and a
lives in a
discrete space, then f
is continuous, and vice versa.
Alias of the forward direction of continuousOn_iff_continuous_restrict
.
If a function is continuous on a set for some topologies, then it is continuous on the same set with respect to any finer topology on the source space.
If a function is continuous on a set for some topologies, then it is continuous on the same set with respect to any coarser topology on the target space.
Alias of the reverse direction of continuousWithinAt_insert_self
.