∀ {ι : Type u_5} {κ : Type u_6} {X : Type u_7} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter ι} {𝓖 : Filter κ},
  Filter.Tendsto φ 𝓖 𝓕 → Filter.IsBoundedUnder r 𝓕 f → Filter.IsBoundedUnder r 𝓖 (f ∘ φ)