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.
𝓝 x: the filter of neighborhoods of a point
𝓟 s: the principal filter of a set
𝓝[s] x: the filter
nhds_within x sof neighborhoods of a point
xwithin a set
A function between topological spaces is continuous at a point
x₀ within a subset
f x tends to
f x₀ when
x tends to
x₀ while staying within
If a function is continuous within
x, then it tends to
f x within
s by definition.
We register this fact for use with the dot notation, especially to use
continuous_within_at.comp will have a different meaning.
A function between topological spaces is continuous on a subset
when it's continuous at every point of
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.