Theorems · Theorem · general topology

Filter.EventuallyEq.comp_tendsto

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f f' : α → β},
  f =ᶠ[l] f' → ∀ {g : γ → α} {lc : Filter γ}, Filter.Tendsto g lc l → f ∘ g =ᶠ[lc] f' ∘ g

Defined in

Mathlib.Order.Filter.Tendsto

Cited by

5 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound