prod_top — Mathlib

English

The product of the top subalgebras is the top subalgebra of the product algebra.

Русский

Произведение верхних подпалгебр равно верхней подпалгебре в A × B.

LaTeX

$$$(\\top \\;\\text{in } \\mathrm{NonUnitalStarSubalgebra}\\,R\,A) \\;\\text{prod}\\; (\\top \\;\\text{in } \\mathrm{NonUnitalStarSubalgebra}\\,R\,B) = \\top$$$

Lean4

@[simp]
theorem prod_top : (prod ⊤ ⊤ : NonUnitalStarSubalgebra R (A × B)) = ⊤ := by ext; simp

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