Theorems · Theorem · general topology

Filter.cardinal_iInter_mem

∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ι → Set α},
  Cardinal.mk ι < c → (⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l)

Defined in

Mathlib.Order.Filter.CardinalInter

Cited by

2 results in Mathlib

Foundations

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

Assumes

CardinalInterFilter