Theorems · Theorem · general topology

Filter.Tendsto.comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ},
  Filter.Tendsto g y z → Filter.Tendsto f x y → Filter.Tendsto (g ∘ f) x z

Defined in

Mathlib.Order.Filter.Tendsto

Cited by

560 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 74 definitions · uses propext, Quot.sound