prod_sup — Mathlib

English

For a filter f on α and filters g1, g2 on β, the product distributes over the supremum on the second coordinate: f ×ˢ (g1 ⊔ g2) = (f ×ˢ g1) ⊔ (f ×ˢ g2).

Русский

Для фильтра f на α и фильтров g1, g2 на β произведение распределяется по верхнему пределу во второй координате: f × g1 ⊔ g2 = (f × g1) ⊔ (f × g2).

LaTeX

$$$$f \times (g_1 \sqcup g_2) = (f \times g_1) \sqcup (f \times g_2).$$$$

Lean4

theorem prod_sup (f : Filter α) (g₁ g₂ : Filter β) : f ×ˢ (g₁ ⊔ g₂) = (f ×ˢ g₁) ⊔ (f ×ˢ g₂) := by
  simp only [prod_eq_inf, comap_sup, inf_sup_left]

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