disjoint_atBot_principal_Ici — Mathlib

English

For any x, the bottom filter atBot is disjoint from the principal filter on Ici(x).

Русский

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

LaTeX

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

Lean4

theorem disjoint_atBot_principal_Ici [Preorder α] [NoBotOrder α] (x : α) : Disjoint atBot (𝓟 (Ici x)) :=
  @disjoint_atTop_principal_Iic αᵒᵈ _ _ _

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