ker_def — Mathlib

English

Let f be a filter on a set α. The kernel f.ker consists exactly of those elements that belong to every member of f; in symbols, f.ker = ⋂_{S ∈ f} S, and a ∈ f.ker iff ∀ S ∈ f, a ∈ S.

Русский

Пусть f — фильтр на множество α. Ядро f состоит из тех элементов, которые принадлежат каждому члену фильтра; то есть f.ker = ⋂_{S ∈ f} S, и для элемента a верно: a ∈ f.ker тогда и только тогда, когда ∀ S ∈ f: a ∈ S.

LaTeX

$$$f.ker = \\bigcap_{S \\in f} S$$$

Lean4

theorem ker_def (f : Filter α) : f.ker = ⋂ s ∈ f, s :=
  sInter_eq_biInter

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