map_snd_prod

Mathlib.Order.Filter.Prod

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

English

If f is nontrivial, then map snd (f × g) = g.

Русский

Если f ненулевой, то отображение snd от произведения фильтров равно g.

LaTeX

$$$\text{(NeBot } f) \Rightarrow \mathrm{map}\, \mathrm{Prod.snd}\ (f \times g) = g$$$

Lean4

@[simp]
theorem map_snd_prod (f : Filter α) (g : Filter β) [NeBot f] : map Prod.snd (f ×ˢ g) = g := by rw [prod_comm, map_map];
  apply map_fst_prod

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

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

Разделы

Аффилиация

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