supported_empty — Mathlib

English

If s is the empty set, then the supported subalgebra is the bottom one, i.e., only constant polynomials live there.

Русский

Если s пусто, то поддерживаемая подалгебра равна нижнему элементу; там живут лишь константные многочлены.

LaTeX

$$$$ \mathrm{supported}(R, \emptyset) = \perp $$$$

Lean4

@[simp]
theorem supported_empty : supported R (∅ : Set σ) = ⊥ := by simp [supported_eq_adjoin_X]

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