elemental_id_eq_top — Mathlib

English

The elemental subalgebra generated by the restriction of the identity on s is the whole algebra.

Русский

Элементальная подалгебра, порожденная ограничением идентичной функции на s, является всей алгеброй.

LaTeX

$$$\mathrm{elemental}_{\mathbb{K}}(\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})) = \top.$$$

Lean4

theorem elemental_id_eq_top {𝕜 : Type*} [RCLike 𝕜] (s : Set 𝕜) [CompactSpace s] :
    elemental 𝕜 (ContinuousMap.restrict s (.id 𝕜)) = ⊤ :=
  by
  rw [StarAlgebra.elemental, ← polynomialFunctions.starClosure_topologicalClosure,
    polynomialFunctions.starClosure_eq_adjoin_X]
  congr
  exact Polynomial.toContinuousMap_X_eq_id.symm

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