singleton_mem_pure

Mathlib.Order.Filter.Map

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

English

For any a, the singleton {a} belongs to the pure filter at a: {a} ∈ pure a.

Русский

Для любого элемента a одиночное множество {a} принадлежит чистому фильтру в точке a: {a} ∈ pure a.

LaTeX

$$$ \{a\} \in (\mathrm{pure} \, a) $$$

Lean4

theorem singleton_mem_pure {a : α} : { a } ∈ (pure a : Filter α) :=
  mem_singleton a

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

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

Разделы

Аффилиация

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