Theorems · Theorem · general topology

Filter.mem_iInf

∀ {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α},
  U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Defined in

Mathlib.Order.Filter.Finite

Cited by

1 results in Mathlib

Foundations

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