instContinuousSub

Mathlib.Topology.Algebra.Ring.Real

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

English

The subtraction operation on NNReal is continuous.

Русский

Операция вычитания на \mathbb{R}_{\ge 0} непрерывна.

LaTeX

$$$ (x,y) \mapsto x \dot{-} y$ is continuous on $\mathbb{R}_{\ge 0} \times \mathbb{R}_{\ge 0}$.$$

Lean4

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

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

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

Разделы

Аффилиация

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