prod_top

Mathlib.Order.Filter.Prod

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

English

The product of f with top on β equals the comap by Prod.fst: f ×ˢ ⊤ = f.comap Prod.fst.

Русский

Произведение f с верхним фильтром β равно предобразу по Prod.fst: f ×ˢ ⊤ = f.comap Prod.fst.

LaTeX

$$$f \\timesˢ (\\top : \\mathrm{Filter}(\\beta)) = f^{\\mathrm{comap}}(\\mathrm{Prod.fst})$$$

Lean4

theorem prod_top : f ×ˢ (⊤ : Filter β) = f.comap Prod.fst := by rw [prod_eq_inf, comap_top, inf_top_eq]

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

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

Разделы

Аффилиация

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