Iic_pure

Mathlib.Order.Filter.Ultrafilter.Defs

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

English

The interval Iic below the principal filter contains exactly two elements: the bottom and the principal filter.

Русский

Интервал Iic ниже главного фильтра состоит ровно из двух элементов:Bottom и самого главного фильтра.

LaTeX

$$$ Iic (pure a : Filter \alpha) = {\x, pure a} $$$

Lean4

@[simp]
theorem Iic_pure (a : α) : Iic (pure a : Filter α) = {⊥, pure a} :=
  isAtom_pure.Iic_eq

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

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

Разделы

Аффилиация

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