instContinuousInv₀

Mathlib.Topology.Instances.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.instContinuousInv₀

English

The reciprocal map x ↦ x⁻¹ is continuous on the set of positive rationals, i.e. on ℚ_{>0} (as a subspace of ℚ).

Русский

Обратное отображение x ↦ x⁻¹ непрерывно на множестве положительных рациональных чисел, как подпространстве ℚ.

LaTeX

$$$\mathrm{ContinuousInv}_0(\mathbb{Q}_{\ge 0})$$$

Lean4

instance : ContinuousInv₀ ℚ≥0 :=
  inferInstance

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

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

Разделы

Аффилиация

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