mem_closedBall_zero

Mathlib.Analysis.Seminorm

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

English

Similarly, y ∈ closedBall p 0 r iff p(y) ≤ r.

Русский

Аналогично, y ∈ closedBall p 0 r эквивалентно p(y) ≤ r.

LaTeX

$$$y \\in \\mathrm{closedBall}_p(0,r) \\iff p(y) \\le r$$$

Lean4

theorem mem_closedBall_zero : y ∈ closedBall p 0 r ↔ p y ≤ r := by rw [mem_closedBall, sub_zero]

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

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

Разделы

Аффилиация

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