ball_eq'

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#ball_eq'

English

Ball(y, ε) consists of those x with ∥x / y∥ < ε.

Русский

Шар вокруг y радиуса ε состоит из тех x, для которых ∥x / y∥ < ε.

LaTeX

$$$$ \mathrm{ball}(y, \varepsilon) = \{ x \in E \mid \|x / y\| < \varepsilon \}.$$$$

Lean4

@[to_additive ball_eq]
theorem ball_eq' (y : E) (ε : ℝ) : ball y ε = {x | ‖x / y‖ < ε} :=
  Set.ext fun a => by simp [dist_eq_norm_div]

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

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

Разделы

Аффилиация

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