Theorems · Theorem · general topology

Filter.HasBasis.hasBasis_self_subset

∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop},
  l.HasBasis (fun s => s ∈ l ∧ p s) id → ∀ {V : Set α}, V ∈ l → l.HasBasis (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

3 results in Mathlib

Foundations

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