prod_inf_prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_inf_prod {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} : (f₁ ×ˢ g₁) ⊓ (f₂ ×ˢ g₂) = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂) := by
  simp only [prod_eq_inf, comap_inf, inf_comm, inf_assoc, inf_left_comm]

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