mem_ball_zero

Mathlib.Analysis.Seminorm

URI: https://scilib.ai/kg/mathlib#Seminorm.mem_ball_zero

English

For any p, y is in ball p 0 r if and only if p(y) < r.

Русский

Для любого p, y принадлежит ball p 0 r тогда и только тогда, когда p(y) < r.

LaTeX

$$$y \\in \\mathrm{ball}_p(0,r) \\iff p(y) < r$$$

Lean4

theorem mem_ball_zero : y ∈ ball p 0 r ↔ p y < r := by rw [mem_ball, sub_zero]

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

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

Разделы

Аффилиация

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