le_pure_iff'

Mathlib.Order.Filter.Ultrafilter.Defs

URI: https://scilib.ai/kg/mathlib#Filter.le_pure_iff'

English

A filter below a principal filter is either bottom or equal to that principal filter.

Русский

Фильтр ниже главного фильтра либо нулевой, либо равен этому главному фильтру.

LaTeX

$$$ f \le pure a \iff f = \bot \lor f = pure a $$$

Lean4

theorem le_pure_iff' : f ≤ pure a ↔ f = ⊥ ∨ f = pure a :=
  isAtom_pure.le_iff

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

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

Разделы

Аффилиация

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