inf_prod — Mathlib

English

For any f₁,f₂ : Filter α and g : Filter β, the product with the infimum in α distributes: (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g).

Русский

Для фильтров f₁,f₂ на α и g на β выполняется: (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g).

LaTeX

$$$ (f_{1} \\wedge f_{2}) \\times\\! g = (f_{1} \\times\\! g) \\wedge (f_{2} \\times\\! g) $$$

Lean4

theorem inf_prod {f₁ f₂ : Filter α} : (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g) := by rw [prod_inf_prod, inf_idem]

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