lt_pure_iff

Mathlib.Order.Filter.Ultrafilter.Defs

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

English

In the filter lattice, f is strictly below pure a iff f = ⊥.

Русский

В решетке фильтров f строго ниже pure a тогда, когда f = ⊥.

LaTeX

$$$ f < pure a \iff f = \bot $$$

Lean4

@[simp]
theorem lt_pure_iff : f < pure a ↔ f = ⊥ :=
  isAtom_pure.lt_iff

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

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

Разделы

Аффилиация

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