hasBasis_pi_principal — Mathlib

English

HasBasis for pi of pure filters is given by finite supports with equality on I.

Русский

У HasBasis для pi чистых фильтров задаётся конечной поддержкой и равенством на I.

LaTeX

$$$\text{hasBasis}(\pi i, pure(f_i)) \Rightarrow \text{HasBasis}$$$

Lean4

/-- The indexed product of a (possibly, infinite) family of principal filters
is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters
is a principal filter, see `pi_principal`. -/
theorem hasBasis_pi_principal (s : (i : ι) → Set (α i)) : HasBasis (pi fun i ↦ 𝓟 (s i)) Set.Finite (Set.pi · s) :=
  ⟨fun _ ↦ mem_pi_principal⟩

Похожие утверждения