Neighborhoods and continuity relative to a subset #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.