ker_iInf — Mathlib

English

For a family of filters (f i), ker of their infimum equals the intersection of all kernels: ker (⨅ i, f i) = ⋂ i, ker (f i).

Русский

Для семейства фильтров (f i) ядро их пересечения равно пересечению всех ядер: ker(⨅ i, f i) = ⋂ i, ker(f i).

LaTeX

$$$\\ker\\big(\\iInf i, f_i\\big) = \\bigcap_i \\ker(f_i)$$$

Lean4

@[simp]
theorem ker_iInf (f : ι → Filter α) : ker (⨅ i, f i) = ⋂ i, ker (f i) :=
  gi_principal_ker.gc.u_iInf

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