instIsTopologicalSemiring

Mathlib.Topology.Instances.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.instIsTopologicalSemiring

← MathLib Explorer

English

ℚ≥0 is a topological semiring.

Русский

ℚ≥0 является топологическим полускольцом.

LaTeX

$$$\\operatorname{IsTopologicalSemiring}(\\mathbb{Q}_{\\ge 0})$$$

Lean4

instance : IsTopologicalSemiring ℚ≥0
    where
  toContinuousAdd := continuousAdd_induced Nonneg.coeRingHom
  toContinuousMul := continuousMul_induced Nonneg.coeRingHom

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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