prod_iInf_left — Mathlib

English

Assume a nonempty index set I. Then (⊓_i f_i) ×ˢ g = ⊓_i (f_i ×ˢ g) for filters f_i on α and g on β.

Русский

Пусть I непусто. Тогда (⊓_i f_i) ×ˢ g = ⊓_i (f_i ×ˢ g) для фильтров f_i на α и g на β.

LaTeX

$$$$\Big(\bigwedge_{i} f_i\Big) \times g = \bigwedge_{i} (f_i \times g).$$$$

Lean4

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

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