Theorems · Theorem · general topology

Filter.IsBasis.mem_filter_iff

∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α},
  U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

1 results in Mathlib

Foundations

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