disjoint_atBot_principal_Ioi — Mathlib

English

For any x in a preordered set, the bottom filter atBot is disjoint from the principal filter generated by the open ray Ioi(x). Equivalently, there exist A ∈ atBot and B ∈ principal(Ioi(x)) with A ∩ B = ∅.

Русский

Для любого x в частично упорядоченном множестве фильтр atBot несовместим с главному фильтру, порождаемому лучом Ioi(x). Существуют A ∈ atBot и B ∈ principal(Ioi(x)) такие, что A ∩ B = ∅.

LaTeX

$$$\mathrm{Disjoint}(\mathrm{atBot}, \mathrm{principal}(\mathrm{Ioi}(x)))$$$

Lean4

theorem disjoint_atBot_principal_Ioi [Preorder α] (x : α) : Disjoint atBot (𝓟 (Ioi x)) :=
  disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl) (Iic_mem_atBot x) (mem_principal_self _)

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