ker

Mathlib.Order.Filter.Defs

URI: https://scilib.ai/kg/mathlib#Filter.ker

English

The kernel of a filter is the intersection of all its sets.

Русский

Кернель фильтра — пересечение всех его множеств.

LaTeX

$$$\mathrm{ker}(f) = \bigcap_0 f.sets$$$

Lean4

/-- The *kernel* of a filter is the intersection of all its sets. -/
def ker (f : Filter α) : Set α :=
  ⋂₀ f.sets

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru