elemental_eq_top — Mathlib

English

The elemental real-valued subalgebra generated by id is the whole, i.e., equals top.

Русский

Элементальная вещественная подалгебра, порожденная id, равна полной алгебре.

LaTeX

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

Lean4

theorem elemental_eq_top {𝕜 : Type*} [RCLike 𝕜] (s : Set 𝕜) [Fact (0 ∈ s)] [CompactSpace s] :
    elemental 𝕜 (ContinuousMapZero.id s) = ⊤ :=
  SetLike.ext'_iff.mpr (adjoin_id_dense s).closure_eq

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