Theorems · Theorem · general topology

Filter.mem_cardinalGenerate_iff

∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s : Set α} {hreg : c.IsRegular},
  s ∈ Filter.cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, Cardinal.mk ↑S < c ∧ ⋂₀ S ⊆ s

A set is in the cardinalInterFilter generated by g if and only if it contains an intersection of c elements of g.

Defined in

Mathlib.Order.Filter.CardinalInter

Cited by

0 results in Mathlib

Foundations

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