sup_prod — Mathlib

English

Let f1, f2 be filters on α and g a filter on β. Then the join of f1 and f2 distributes over the product with g: (f1 ⊔ f2) ×ˢ g = (f1 ×ˢ g) ⊔ (f2 ×ˢ g).

Русский

Пусть f1, f2 — фильтры на α и g — фильтр на β. Тогда объединение f1 и f2 распределяется над произведением с g: (f1 ⊔ f2) × g = (f1 × g) ⊔ (f2 × g).

LaTeX

$$$$(f_1 \sqcup f_2) \times g = (f_1 \times g) \sqcup (f_2 \times g).$$$$

Lean4

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

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