Neighborhoods and continuity relative to a subset #
This file develops API on the relative versions
related to continuity, which are defined in previous definition files. Their basic properties studied in this file include 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
.
Properties of the neighborhood-within filter #
Alias of eventually_eventually_nhdsWithin
.
If L
and R
are neighborhoods of b
within sets whose union is Set.univ
, then
L ∪ R
is a neighborhood of b
.
Writing a punctured neighborhood filter as a sup of left and right filters.
Obtain a "predictably-sided" neighborhood of b
from two one-sided neighborhoods.
Alias of Filter.EventuallyEq.mem_interior_iff
.
nhdsWithin
and subtypes #
Local continuity properties of functions #
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.
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.
Congruence and monotonicity properties with respect to sets #
If two sets coincide around x
, then being continuous within one or the other at x
is
equivalent. See also continuousWithinAt_congr_set'
which requires that the sets coincide
locally away from a point y
, in a T1 space.
Alias of continuousWithinAt_congr_set
.
If two sets coincide around x
, then being continuous within one or the other at x
is
equivalent. See also continuousWithinAt_congr_set'
which requires that the sets coincide
locally away from a point y
, in a T1 space.
Alias of ContinuousWithinAt.congr_set
.
Alias of the reverse direction of continuousWithinAt_insert_self
.
Alias of the reverse direction of continuousWithinAt_insert_self
.
Alias of the reverse direction of continuousWithinAt_insert_self
.
See also continuousWithinAt_diff_singleton
for the case of s \ {y}
, but
requiring `T1Space α.
Relation between ContinuousAt
and ContinuousWithinAt
#
Alias of continuousOn_of_forall_continuousAt
.
Congruence properties with respect to functions #
Composition #
Alias of ContinuousWithinAt.comp_inter
.
See also ContinuousOn.comp'
using the form fun y ↦ g (f y)
instead of g ∘ f
.
Variant of ContinuousOn.comp
using the form fun y ↦ g (f y)
instead of g ∘ f
.
See also Continuous.comp_continuousOn'
using the form fun y ↦ g (f y)
instead of g ∘ f
.
Variant of Continuous.comp_continuousOn
using the form fun y ↦ g (f y)
instead of g ∘ f
.
Image #
Product #
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.
Pi #
Specific functions #
Alias of Topology.IsInducing.continuousOn_iff
.
Alias of Topology.IsEmbedding.continuousOn_iff
.
Alias of Topology.IsEmbedding.map_nhdsWithin_eq
.
Alias of Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq
.
Continuity of piecewise defined functions #
If f
is continuous on an open set s
and continuous at each point of another
set t
then f
is continuous on s ∪ t
.