English
In a dense inducing diagram, if h tends to i(a) along nhds b and h∘g = i∘f, then f tends to a along comap g (nhds b).
Русский
В диаграмме плотного индуцирования, если h стремится к i(a) вдоль nhds b и h∘g = i∘f, то f стремится к a вдоль comap g (nhds b).
LaTeX
$$$\\text{DenseInducing}(i) \\to \\Big( \\text{Tendsto } h (\\mathcal{N} d) (\\mathcal{N}(i a)) \\land (h \\circ g = i \\circ f) \\Rightarrow \\text{Tendsto } f (\\operatorname{comap} g (\\mathcal{N} d)) (\\mathcal{N} a) \\Big$$$
Lean4
/-- ```
γ -f→ α
g↓ ↓e
δ -h→ β
```
-/
theorem tendsto_comap_nhds_nhds {d : δ} {a : α} (di : IsDenseInducing i) (H : Tendsto h (𝓝 d) (𝓝 (i a)))
(comm : h ∘ g = i ∘ f) : Tendsto f (comap g (𝓝 d)) (𝓝 a) :=
by
have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le
replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1
rw [Filter.map_map, comm, ← Filter.map_map, map_le_iff_le_comap] at lim1
have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a)) := comap_mono H
rw [← di.nhds_eq_comap] at lim2
exact le_trans lim1 lim2
