div₀

Mathlib.Topology.Algebra.GroupWithZero

URI: https://scilib.ai/kg/mathlib#ContinuousAt.div₀

← MathLib Explorer

English

The equality 𝓝(x⁻¹) = (𝓝(x))⁻¹ holds for x ≠ 0 in a group with zero.

Русский

Равенство 𝓝(x⁻¹) = (𝓝(x))⁻¹ справедливо для x ≠ 0 в группе с нулём.

LaTeX

$$𝓝(x^{-1}) = (𝓝(x))^{-1} \\quad (x \\neq 0)$$

Lean4

@[fun_prop]
theorem div₀ (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) : ContinuousAt (fun x => f x / g x) a :=
  ContinuousAt.div hf hg h₀

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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