Theorems · Theorem · general topology

Filter.HasAntitoneBasis.map

∀ {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
  l.HasAntitoneBasis s → ∀ (m : α → β), (Filter.map m l).HasAntitoneBasis fun x => m '' s x

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Preorder