Theorems · Theorem · general topology

Filter.HasBasis.congr

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

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

7 results in Mathlib

Foundations

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