le_prod_map_fst_snd

Mathlib.Order.Filter.Prod

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

English

For any f on α×β, f ≤ map fst f × map snd f.

Русский

Для любого фильтра f на α×β верно f ≤ map fst f × map snd f.

LaTeX

$$$f \le \mathrm{map}\ \mathrm{Prod.fst} f \times\! \mathrm{map}\ \mathrm{Prod.snd} f$$$

Lean4

theorem le_prod_map_fst_snd {f : Filter (α × β)} : f ≤ map Prod.fst f ×ˢ map Prod.snd f :=
  le_inf le_comap_map le_comap_map

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

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

Разделы

Аффилиация

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