supported_univ — Mathlib

English

For a commutative semiring R, the supported subalgebra on the universal set equals the top element: supported R Set.univ = ⊤.

Русский

Для коммутативного полусурья R поддерживаемое по всем переменным множество равно вершине: supported R Set.univ = ⊤.

LaTeX

$$$\\mathrm{supported}\\ R\\ \\mathrm{Set.univ} = \\top$$$

Lean4

@[simp]
theorem supported_univ : supported R (Set.univ : Set σ) = ⊤ := by simp [Algebra.eq_top_iff, mem_supported]

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