prod_iInf_right

Mathlib.Order.Filter.Prod

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

← MathLib Explorer

English

Similarly, f ×ˢ (⊓_i g_i) = ⊓_i (f ×ˢ g_i) for a fixed f and family g_i.

Русский

Аналогично, f ×ˢ (⊓_i g_i) = ⊓_i (f ×ˢ g_i).

LaTeX

$$$$f \times g = \bigwedge_i (f \times g_i).$$$$

Lean4

theorem prod_iInf_right [Nonempty ι] {f : Filter α} {g : ι → Filter β} : (f ×ˢ ⨅ i, g i) = ⨅ i, f ×ˢ g i := by
  simp only [prod_eq_inf, comap_iInf, inf_iInf]

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

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

Разделы

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

Аффилиация

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