frontier_ball_subset_sphere

Mathlib.Topology.MetricSpace.Pseudo.Lemmas

URI: https://scilib.ai/kg/mathlib#Metric.frontier_ball_subset_sphere

← MathLib Explorer

English

The boundary of a ball is contained in the corresponding sphere.

Русский

Граница шара содержится в соответствующей сфере.

LaTeX

$$$\text{frontier}(\mathrm{ball}(x,\varepsilon)) \subseteq \mathrm{sphere}(x,\varepsilon)$$$

Lean4

theorem frontier_ball_subset_sphere : frontier (ball x ε) ⊆ sphere x ε :=
  frontier_lt_subset_eq (continuous_id.dist continuous_const) continuous_const

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

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

Разделы

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

Аффилиация

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