frontier_ball_eq_empty

Mathlib.Topology.MetricSpace.Ultra.Basic

URI: https://scilib.ai/kg/mathlib#IsUltrametricDist.frontier_ball_eq_empty

English

In an ultrametric space, the frontier of the open ball B(x,r) is empty for r ≠ 0.

Русский

В ультраметрическом пространстве граница открытого шара B(x,r) пустая при r ≠ 0.

LaTeX

$$frontier(\mathrm{ball}(x,r)) = \emptyset$$

Lean4

theorem frontier_ball_eq_empty : frontier (ball x r) = ∅ :=
  isClopen_iff_frontier_eq_empty.mp (isClopen_ball x r)

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

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

Разделы

Аффилиация

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