disjoint_atTop_atBot — Mathlib

English

The top and bottom filters are negations of each other in a disjoint sense; equivalently, atTop and atBot are disjoint in any nontrivial poset.

Русский

Топ и бот фильтры остаются несовместимыми в любом не тривиальном частично упорядоченном множестве.

LaTeX

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

Lean4

theorem disjoint_atTop_atBot [PartialOrder α] [Nontrivial α] : Disjoint (atTop : Filter α) atBot :=
  disjoint_atBot_atTop.symm

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