disjoint_atBot_atTop — Mathlib

English

In a nontrivial partial order, the top and bottom filters are disjoint: atTop and atBot do not share any common sets.

Русский

В непустом частично упорядоченном множестве верхний и нижний фильтры несовместимы: atTop и atBot не имеют общих множеств.

LaTeX

$$$\mathrm{Disjoint}(\mathrm{atTop}, \mathrm{atBot})$$$

Lean4

theorem disjoint_atBot_atTop [PartialOrder α] [Nontrivial α] : Disjoint (atBot : Filter α) atTop :=
  by
  rcases exists_pair_ne α with ⟨x, y, hne⟩
  by_cases hle : x ≤ y
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)
    exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
    exact Iic_disjoint_Ici.2 hle

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