map_atBot_eq — Mathlib

English

For a function f: α→β, the image of the bottom filter atBot under f equals the infimum over a of the principal filters generated by the images of downward-closed sets {a' | a' ≤ a}.

Русский

Для отображения f: α→β произведение фильтра atBot над mапом f равно инфимууму по a от главных фильтров, порождаемых образами множеств {a' | a' ≤ a}.

LaTeX

$$$ atBot.map f = \bigwedge_{a\in α} 𝓟 (f''\{a'\mid a'\le a\})$$$

Lean4

theorem map_atBot_eq {f : α → β} : atBot.map f = ⨅ a, 𝓟 (f '' {a' | a' ≤ a}) :=
  map_atTop_eq (α := αᵒᵈ)

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