subsingleton_pure

Mathlib.Order.Filter.Subsingleton

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

English

For any a, the pure filter at a is subsingleton.

Русский

Для любого элемента a чистый фильтр в точке a является подсинглетным.

LaTeX

$$$$ (pure\ a).Subsingleton $$$$

Lean4

@[simp]
theorem subsingleton_pure {a : α} : Filter.Subsingleton (pure a) :=
  ⟨{ a }, rfl, subsingleton_singleton⟩

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

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

Разделы

Аффилиация

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