atBot_Iio_eq — Mathlib

English

Same principle as above: the map along the inclusion from a closed interval into α preserves atTop.

Русский

То же самое: отображение через включение сохраняет atTop.

LaTeX

$$$\mathrm{map}\left(\mathrm{Subtype.val}\right)\mathrm{atTop} = \mathrm{atTop}$$$

Lean4

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

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