prod_inf_prod — Mathlib

English

The infimum (intersection) of product subalgebras equals the product of infima: S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁).

Русский

Пересечение произведений подалгебр равно произведению пересечений.

LaTeX

$$prod_inf_prod : S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)$$

Lean4

@[simp]
theorem prod_inf_prod {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} :
    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
  SetLike.coe_injective Set.prod_inter_prod

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