prod_map_right

Mathlib.Order.Filter.Prod

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

← MathLib Explorer

English

F × map f G = map (Prod.map id f) (F × G).

Русский

F × map f G = map (Prod.map id f) (F × G).

LaTeX

$$$F \times\! \mathrm{map}\ f\ G = \mathrm{map}\ (\mathrm{Prod.map}\ id\ f)\ (F \times\! G)$$$

Lean4

theorem prod_map_right (f : β → γ) (F : Filter α) (G : Filter β) : F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G) := by
  rw [← prod_map_map_eq', map_id]

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

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

Разделы

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

Аффилиация

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