prod_inf — Mathlib

English

For any f : Filter α and g₁,g₂ : Filter β, the meet distributes over the product in the second factor: f ×ˢ (g₁ ⊓ g₂) = (f ×ˢ g₁) ⊓ (f ×ˢ g₂).

Русский

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

LaTeX

$$$ f \\times\\! (g_{1} \\wedge g_{2}) = (f \\times\\! g_{1}) \\wedge (f \\times\\! g_{2}) $$$

Lean4

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

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