Theorems · Theorem · general topology

Filter.pi_principal

∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] (s : (i : ι) → Set (α i)),
  (Filter.pi fun i => Filter.principal (s i)) = Filter.principal (Set.univ.pi s)

The indexed product of finitely many principal filters is the principal filter corresponding to the cylinder Set.univ.pi s. If the index type is infinite, then mem_pi_principal and hasBasis_pi_principal may be useful.

Defined in

Mathlib.Order.Filter.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

Finite