Theorems · Theorem · general topology

Filter.HasBasis.ext

∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s →
    l'.HasBasis p' s' →
      (∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) → (∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') → l = l'

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

6 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound