map_inv'

Mathlib.Order.Filter.Pointwise

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

English

For any map m, the image of the inverse of f equals the inverse of the image: map_inv' holds.

Русский

При любом отображении m образ обратного фильтра равен обратному образу отображения: map_inv'.

LaTeX

$$f^{-1}.map m = (f.map m)^{-1}$$

Lean4

@[to_additive]
theorem map_inv' : f⁻¹.map m = (f.map m)⁻¹ :=
  Semiconj.filter_map (map_inv m) f

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

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

Разделы

Аффилиация

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