instPure

Mathlib.Order.Filter.Defs

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

← MathLib Explorer

English

The kernel ker(f) is the intersection of all sets in f.

Русский

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

LaTeX

$$$\mathrm{ker}(f) = \bigcap_{s\in f.sets} s$$$

Lean4

/-- `pure x` is the set of sets that contain `x`. It is equal to `𝓟 {x}` but
with this definition we have `s ∈ pure a` defeq `a ∈ s`. -/
instance : Pure Filter where pure x := .copy (𝓟 { x }) {s | x ∈ s} fun _ ↦ by simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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