English
Let f be an ultrafilter on a set α and m: α → β. Then the ultrafilter on β obtained by mapping along m has as its underlying filter exactly the pushforward of the underlying filter of f by m; i.e. the corresponding filters agree: (map m f) as a Filter β equals Filter.map m applied to the underlying Filter of f.
Русский
Пусть f — ультрафильтр на α и m: α → β. Тогда ультрафильтр на β, полученный отображением по m, имеет в основе тот же переходной фильтр: (map m f) как фильтр β совпадает с Filter.map m от базового фильтра f.
LaTeX
$$$ (map m f : Filter \beta) = Filter.map m \uparrow f $$$
Lean4
@[simp, norm_cast]
theorem coe_map (m : α → β) (f : Ultrafilter α) : (map m f : Filter β) = Filter.map m ↑f :=
rfl
