map_atTop_eq — Mathlib

English

The map of atTop under f equals the infimum of the principal filters generated by the image of f on initial tails.

Русский

Образ фильтра atTop через отображение f равен инфимуму основанных на образе f для хвостов.

LaTeX

$$$ atTop.map f = \\bigwedge_{a} \\mathcal{P}\\bigl(f''\\{a' \\mid a' \\ge a\\}\\bigr)$$$

Lean4

theorem map_atTop_eq {f : α → β} : atTop.map f = ⨅ a, 𝓟 (f '' {a' | a ≤ a'}) :=
  (atTop_basis.map f).eq_iInf

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