disjoint_atTop_principal_Iic — Mathlib

English

For any x in a preorder with no-top, the top filter atTop is disjoint from the principal filter on Iic(x).

Русский

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

LaTeX

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

Lean4

theorem disjoint_atTop_principal_Iic [Preorder α] [NoTopOrder α] (x : α) : Disjoint atTop (𝓟 (Iic x)) :=
  disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl).symm (Ioi_mem_atTop x) (mem_principal_self _)

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