mem_closedBall_self

Mathlib.Analysis.Seminorm

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

English

If 0 ≤ r, then x lies in the closedBall p x r for any seminorm p.

Русский

Если 0 ≤ r, то x принадлежит closedBall p x r для любого семинормa.

LaTeX

$$$x \\in \\mathrm{closedBall}_p(x,r)$ при условии $0 \\le r$$$

Lean4

theorem mem_closedBall_self (hr : 0 ≤ r) : x ∈ closedBall p x r := by simp [hr]

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

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

Разделы

Аффилиация

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