atBot_eq — Mathlib

English

Dual statement: in a poset with a bottom element, the atBot filter equals the principal filter generated by the bottom element.

Русский

Двойственное утверждение: в частично упорядоченном множестве с нижним элементом фильтр atBot совпадает с простым фильтром, порождённым нижним элементом.

LaTeX

$$$$\text{atBot} = \text{pure}(\bot).$$$$

Lean4

theorem atBot_eq (α) [PartialOrder α] [OrderBot α] : (atBot : Filter α) = pure ⊥ :=
  @OrderTop.atTop_eq αᵒᵈ _ _

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