atBot_Iic_eq — Mathlib

English

The atBot filter for Iio a is the same as the ambient atBot under the dual order.

Русский

Фильтр atBot для Iio a совпадает с фильтром atBot в основном порядке двойственности.

LaTeX

$$$\mathrm{atBot} = \mathrm{comap}(\uparrow)\mathrm{atBot}$$$

Lean4

/-- The `atBot` filter for an open interval `Iic a` comes from the `atBot` filter in the ambient
order. -/
theorem atBot_Iic_eq [Preorder α] [IsDirected α (· ≥ ·)] (a : α) : atBot = comap ((↑) : Iic a → α) atBot :=
  atTop_Ici_eq (OrderDual.toDual a)

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