disjoint_pure_atTop — Mathlib

English

The pure filter at a point x is disjoint from the top filter atTop. In particular, there exist a set in pure x and a set in atTop that are disjoint.

Русский

Пусть чистый фильтр при x несовместим с верхним фильтром atTop; существует множество в чистом фильтре при x и множество в atTop, которые не пересекаются.

LaTeX

$$$\mathrm{Disjoint}(\mathrm{pure}(x), \mathrm{atTop})$$$

Lean4

theorem disjoint_pure_atTop [Preorder α] [NoTopOrder α] (x : α) : Disjoint (pure x) atTop :=
  Disjoint.symm <| (disjoint_atTop_principal_Iic x).mono_right <| le_principal_iff.2 <| mem_pure.2 right_mem_Iic

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