map_equiv_symm

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_equiv_symm

← MathLib Explorer

English

For an equivalence e, map e.symm f equals comap e f.

Русский

Для эквивалентности e отображение e.symm применимо к f равно обратному образу f по e.

LaTeX

$$map e.symm f = comap e f$$

Lean4

theorem map_equiv_symm (e : α ≃ β) (f : Filter β) : map e.symm f = comap e f :=
  map_injective e.injective <| by rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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