div

Mathlib.Analysis.Normed.Group.Pointwise

URI: https://scilib.ai/kg/mathlib#Bornology.IsBounded.div

English

Same as 54259 but in plain real norm.

Русский

То же, что и в 54259, в обычной норме.

LaTeX

$$$\forall x_0\in E\,\forall ε>0\, \forall^{\infty} x\in 𝓝 x_0, \|x- x_0\| < ε$$$

Lean4

@[to_additive]
theorem div (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s / t) :=
  div_eq_mul_inv s t ▸ hs.mul ht.inv

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

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

Разделы

Аффилиация

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