pi_top — Mathlib

English

For any index set s, the pi construction with the top subalgebras in every coordinate yields the top subalgebra of the product.

Русский

Для множества индексов s конструктор π над верхними подалгебрами в каждой координате даёт верхнюю подалгебру произведения.

LaTeX

$$$\pi(s,\top) = \top$$$

Lean4

@[simp]
theorem pi_top (s : Set ι) : pi s (fun i ↦ (⊤ : Subalgebra R (S i))) = ⊤ :=
  SetLike.coe_injective <| Set.pi_univ _

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