Theorems · Theorem · general topology

Filter.HasAntitoneBasis.comp_mono

∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Nonempty ι] [inst : Preorder ι] [IsDirectedOrder ι]
  [inst_2 : Preorder ι'] {l : Filter α} {s : ι' → Set α},
  l.HasAntitoneBasis s →
    ∀ {φ : ι → ι'}, Monotone φ → Filter.Tendsto φ Filter.atTop Filter.atTop → l.HasAntitoneBasis (s ∘ φ)

Defined in

Mathlib.Order.Filter.AtTopBot.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonemptyPreorderIsDirectedOrderPreorder