English
Detailed equivalences for mem_pi_pure and related lemmas.
Русский
Детальные эквивалентности mem_pi_pure и связанные леммы.
LaTeX
$$$\text{...}$$$
Lean4
/-- The indexed product of a (possibly, infinite) family of pure filters `pure (f i)`
is generated by the sets of functions that are equal to `f` on a finite set.
If the index type is finite, then the indexed product of pure filters is a pure filter,
see `pi_pure`. -/
theorem mem_pi_pure {f : (i : ι) → α i} {s : Set ((i : ι) → α i)} :
s ∈ pi (fun i ↦ pure (f i)) ↔ ∃ I : Set ι, I.Finite ∧ ∀ g, (∀ i ∈ I, g i = f i) → g ∈ s :=
by
simp only [← principal_singleton, mem_pi_principal]
simp [subset_def]
