ker_pure

Mathlib.Order.Filter.Ker

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

English

The kernel of the pure filter at a is the singleton {a}: ker (pure a) = {a}.

Русский

Ядро чистого фильтра на точке a равно множеству {a}.

LaTeX

$$$\\ker(\\text{pure } a) = \\{ a \\}$$$

Lean4

@[simp]
theorem ker_pure (a : α) : ker (pure a) = { a } := by rw [← principal_singleton, ker_principal]

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

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

Разделы

Аффилиация

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