map_val_Ici_atTop — Mathlib

English

The image of the atTop filter under the projection from Ici a to α remains atTop for any a.

Русский

Образ фильтра atTop под отображением включения из Ici a в α сохраняется как atTop.

LaTeX

$$$\forall a:\alpha,\ \mathrm{map}\bigl(\mathrm{Subtype.val}\bigr)\ \mathrm{Filter.atTop} = \mathrm{Filter.atTop}$$$

Lean4

/-- The image of the filter `atTop` on `Ici a` under the coercion equals `atTop`. -/
@[simp]
theorem map_val_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)] (a : α) : map ((↑) : Ici a → α) atTop = atTop :=
  map_val_atTop_of_Ici_subset Subset.rfl

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