map_id

Mathlib.Order.Filter.Ultrafilter.Defs

URI: https://scilib.ai/kg/mathlib#Ultrafilter.map_id

English

The identity function leaves every ultrafilter unchanged: map id f = f.

Русский

Идентичное отображение не изменяет ультрафильтр: map id f = f.

LaTeX

$$$ f.map id = f $$$

Lean4

@[simp]
nonrec theorem map_id (f : Ultrafilter α) : f.map id = f :=
  coe_injective map_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru