map_val_Iio_atBot — Mathlib

English

If Ici a is contained in a subset s, then the inclusion from s into α carries atTop to atTop.

Русский

Если Ici a ⊆ s, то включение s → α переносит atTop в atTop.

LaTeX

$$$\forall a,\ (Ici\ a \subseteq s)\Rightarrow \mathrm{map}\left(\mathrm{Subtype.mono}\right)\mathrm{atTop} = \mathrm{atTop}$$$

Lean4

/-- The `atBot` filter for an open interval `Iio a` comes from the `atBot` filter in the ambient
order. -/
@[simp]
theorem map_val_Iio_atBot [Preorder α] [IsDirected α (· ≥ ·)] [NoMinOrder α] (a : α) :
    map ((↑) : Iio a → α) atBot = atBot :=
  map_val_Ioi_atTop (OrderDual.toDual a)

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