continuousAt_inv

Mathlib.Analysis.Normed.Field.Lemmas

URI: https://scilib.ai/kg/mathlib#NormedField.continuousAt_inv

English

The inverse map is continuous at a point x precisely when x ≠ 0.

Русский

Обратное отображение непрерывно в точке тогда и только тогда, когда x ≠ 0.

LaTeX

$$$\text{ContinuousAt}(\mathrm{inv}, x) \iff x \neq 0.$$$

Lean4

@[simp]
protected theorem continuousAt_inv : ContinuousAt Inv.inv x ↔ x ≠ 0 := by
  simpa using NormedField.continuousAt_zpow (n := -1) (x := x)

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

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

Разделы

Аффилиация

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