map_val_Ioi_atTop — Mathlib

English

The map of Subtype.val on Filter.atTop for the open interval Ioi a equals atTop.

Русский

Отображение Subtype.val на atTop для открытого интервала Ioi a даёт atTop.

LaTeX

$$$\forall a:\alpha,\ \mathrm{Eq}\left( \mathrm{Filter.map}\ \mathrm{Subtype.val}\ \mathrm{Filter.atTop}, \mathrm{Filter.atTop} \right)$$$

Lean4

/-- The image of the filter `atTop` on `Ioi a` under the coercion equals `atTop`. -/
@[simp]
theorem map_val_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α] (a : α) :
    map ((↑) : Ioi a → α) atTop = atTop :=
  let ⟨_b, hb⟩ := exists_gt a
  map_val_atTop_of_Ici_subset <| Ici_subset_Ioi.2 hb

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