instT2SpaceHomOfCarrier

Mathlib.Algebra.Category.Ring.Topology

URI: https://scilib.ai/kg/mathlib#CommRingCat.HomTopology.instT2SpaceHomOfCarrier

English

If R is a topological ring, then the function space Hom(A,R) is a T2 space when R is T2.

Русский

Если R — топологическое кольцо, тогда пространство функций Hom(A,R) является T2, когда R T2.

LaTeX

$$$[IsTopologicalRing\, R] \Rightarrow [T2Space(R) \Rightarrow T2Space(A \to R)]$$$

Lean4

instance [T2Space R] : T2Space (A ⟶ R) :=
  (isEmbedding_hom R A).t2Space

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

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

Разделы

Аффилиация

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