instContinuousSub

Mathlib.Topology.Instances.Rat

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

English

There is a continuous substructure on ℚ≥0.

Русский

Существует непрерывная подструктура на ℚ≥0.

LaTeX

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

Lean4

instance : ContinuousSub ℚ≥0 :=
  ⟨((continuous_subtype_val.fst'.sub continuous_subtype_val.snd').max continuous_const).subtype_mk _⟩

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

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

Разделы

Аффилиация

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