Theorems · Theorem · general topology

IsExtrFilter.comp_tendsto

∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
  {b : δ}, IsExtrFilter f l (g b) → Filter.Tendsto g l' l → IsExtrFilter (f ∘ g) l' b

Defined in

Mathlib.Order.Filter.Extr

Cited by

2 results in Mathlib

Foundations

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

Assumes

Preorder