prod_map_left

Mathlib.Order.Filter.Prod

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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