continuous_inv

Mathlib.Topology.Instances.Real.Lemmas

URI: https://scilib.ai/kg/mathlib#Real.continuous_inv

English

The inversion map r ↦ r⁻¹ is continuous on the subset { r ∈ ℝ | r ≠ 0 }.

Русский

Обратная карта r ↦ r⁻¹ непрерывна на множестве { r ∈ ℝ | r ≠ 0 }.

LaTeX

$$$\text{continuous}^{-1} : \{ r \in \mathbb{R} \mid r \neq 0 \} \to \mathbb{R}, \ r \mapsto r^{-1}$ is continuous.$$

Lean4

theorem continuous_inv : Continuous fun a : { r : ℝ // r ≠ 0 } => a.val⁻¹ :=
  continuousOn_inv₀.restrict

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

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

Разделы

Аффилиация

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