Theorems · Theorem · general topology

Filter.mem_biInf_principal

∀ {α : Type u} {ι : Type u_2} {p : ι → Prop} {s : ι → Set α} {t : Set α},
  t ∈ ⨅ i, ⨅ (_ : p i), Filter.principal (s i) ↔ ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

Defined in

Mathlib.Order.Filter.Finite

Cited by

0 results in Mathlib

Foundations

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