ker_sInf — Mathlib

English

For a set S of filters, ker of their infimum (sInf S) equals the intersection over S of the kernels: ker (sInf S) = ⋂ f ∈ S, ker f.

Русский

Для множества фильтров S ядро их пересечения равно пересечению ядер всех элементов S: ker (sInf S) = ⋂ f ∈ S, ker f.

LaTeX

$$$\\ker(\\mathrm{sInf}\\,S) = \\bigcap_{f \\in S} \\ker f$$$

Lean4

@[simp]
theorem ker_sInf (S : Set (Filter α)) : ker (sInf S) = ⋂ f ∈ S, ker f :=
  gi_principal_ker.gc.u_sInf

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