ker_pi — Mathlib

English

For a family of filters f over α indexed by ι, ker of the Pi-filter equals the Pi of kernels: ker (Filter.pi f) = univ.pi (λ i, ker (f i)).

Русский

Для семейства фильтров f над α индекса ι ядро фильтра-произведения равно произведению ядер f_i: ker(pi f) = univ.pi (λ i, ker(f i)).

LaTeX

$$$\\ker(\\text{Filter.pi}\, f) = \\text{univ.pi} \\big(\\lambda i. \\ker(f(i))\\big)$$$

Lean4

@[simp]
theorem ker_pi {ι : Type*} {α : ι → Type*} (f : (i : ι) → Filter (α i)) :
    ker (Filter.pi f) = univ.pi (fun i => ker (f i)) := by simp [Set.pi_def, Filter.pi]

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