disjoint_atTop_principal_Iio — Mathlib

English

For any x in a preorder, the top filter atTop is disjoint from the principal filter generated by the interval Iio(x).

Русский

Для любого x в частично упорядоченном множестве фильтр atTop несовместим с главному фильтру, порождаемому интервалом Iio(x).

LaTeX

$$$\mathrm{Disjoint}(\mathrm{atTop}, \mathrm{principal}(\mathrm{Iio}(x)))$$$

Lean4

theorem disjoint_atTop_principal_Iio [Preorder α] (x : α) : Disjoint atTop (𝓟 (Iio x)) :=
  @disjoint_atBot_principal_Ioi αᵒᵈ _ _

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