tendsto_induced

Stream: Is there code for X?

[Kalle Kytölä]

Do we have the following or something that easily implies it? I could not find it by library_search or in what I thought were the obvious places to look.

import topology.constructions

open filter
open_locale topological_space

lemma tendsto_induced {α β δ : Type*} [topo_β : topological_space β] (F : filter δ)
  (f : α → β) (x : δ → α) (x₀ : α) (h_f_tends : tendsto (f ∘ x) F (𝓝 (f(x₀)))) :
  tendsto x F (@nhds α (topological_space.induced f topo_β) x₀) :=
begin
  apply tendsto_nhds.mpr,
  intros U open_U U_ni_x₀,
  rcases ((@is_open_induced_iff α β topo_β U f).mp open_U) with ⟨ V , open_V , preim_V_eq_U ⟩,
  induction preim_V_eq_U,
  apply tendsto_nhds.mp h_f_tends V open_V U_ni_x₀,
end

[Heather Macbeth]

If you're willing to abuse definitional equality a bit, the following works:

begin
  rw nhds_induced,
  exact map_le_iff_le_comap.mp h_f_tends
end

[Heather Macbeth]

Oh ... and docs#filter.tendsto_comap_iff is apparently how to do it without such abuse.

by rwa [nhds_induced, tendsto_comap_iff]

[Kalle Kytölä]

Wow, thank you very much again!

(...and I'd anyway be more than willing to abuse definitional equality. The goals accomplished justify the means, is what they say if I remember right.)