This file defines relative versions
nhds_within of nhds continuous_on of continuous continuous_within_at of continuous_at
and proves their basic properties, including the relationships between these restricted notions and the corresponding notions for the subtype equipped with the subspace topology.
The "neighborhood within" filter. Elements of nhds_within a s are sets containing the intersection of s and a neighborhood of a.
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.
A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s.