frontier_ball

Mathlib.Analysis.Normed.Module.RCLike.Real

URI: https://scilib.ai/kg/mathlib#frontier_ball

← MathLib Explorer

English

The boundary of an open ball is the corresponding sphere.

Русский

Граница открытого шара есть соответствующая сфера.

LaTeX

$$$\\operatorname{frontier}(\\operatorname{Ball}(x,r)) = \\operatorname{Sphere}(x,r)$$$

Lean4

theorem frontier_ball (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (ball x r) = sphere x r := by
  rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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