Local images of open sets under inducing maps #
An open neighborhood in the source of an inducing map agrees, near the image of each of its points, with the full range of the map.
theorem
TauCeti.exists_ball_inter_range_eq_ball_inter_image_of_isInducing
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[PseudoMetricSpace Y]
(f : X → Y)
(hf : Topology.IsInducing f)
{s : Set X}
(hs : IsOpen s)
{x : X}
(hx : x ∈ s)
:
∃ (ε : ℝ), 0 < ε ∧ Metric.ball (f x) ε ∩ Set.range f = Metric.ball (f x) ε ∩ f '' s
Near the image of a point in an open set, the range of an inducing map agrees with the image of that open set.