Theorems · Theorem · general topology

Filter.HasBasis.comap

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : β → α),
  l.HasBasis p s → (Filter.comap f l).HasBasis p fun i => f ⁻¹' s i

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

89 results in Mathlib

Foundations

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