Theorems · Theorem · general topology

Filter.Tendsto.of_tendsto_comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {a : Filter α} {b : Filter β} {c : Filter γ},
  Filter.Tendsto (g ∘ f) a c → Filter.comap g c ≤ b → Filter.Tendsto f a b

Defined in

Mathlib.Order.Filter.Tendsto

Cited by

4 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound