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 filternhds_within x s
of neighborhoods of a pointx
within a sets
.
nhds_within
and subtypes
A function between topological spaces is continuous at a point x₀
within a subset s
if f x
tends to f x₀
when x
tends to x₀
while staying within s
.
Equations
- continuous_within_at f s x = filter.tendsto f (𝓝[s] x) (𝓝 (f x))
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 tendsto.comp
as
continuous_within_at.comp
will have a different meaning.
A function between topological spaces is continuous on a subset s
when it's continuous at every point of s
within s
.
Equations
- continuous_on f s = ∀ (x : α), x ∈ s → continuous_within_at f s x
Alias of continuous_within_at_insert_self
.