id

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousAlgHom.id

English

The underlying set of topologicalClosure of a subalgebra equals the topological closure of its underlying set.

Русский

Носитель подалгебры topologicalClosure равен замыканию носителя подалгебры.

LaTeX

$$(s.topologicalClosure : Set A) = closure ↑s$$

Lean4

/-- The identity map as a continuous algebra homomorphism. -/
protected def id : A →A[R] A :=
  ⟨AlgHom.id R A, continuous_id⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru