prod_inf_prod — Mathlib

English

The infimum (greatest lower bound) of product subalgebras equals the product of infima: S.prod S₁ ∧ T.prod T₁ = (S ∧ T).prod (S₁ ∧ T₁).

Русский

Грань произведения подпалгебр равна произведению граней: 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 : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} :
    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
  SetLike.coe_injective Set.prod_inter_prod

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