map_id'

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_id'

English

The variant with a trivial function yields the same result as map_id: map (fun x => x) f = f.

Русский

Вариант с тривиальной функцией дает то же самое, что и map_id: map (fun x => x) f = f.

LaTeX

$$map_id' : map (fun x => x) f = f$$

Lean4

@[simp]
theorem map_id' : Filter.map (fun x => x) f = f :=
  map_id

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

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

Разделы

Аффилиация

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