isClopen_ball

Mathlib.Topology.MetricSpace.Ultra.Basic

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

English

In an ultrametric space, every ball is clopen (both open and closed).

Русский

В ультраметрическом пространстве любая сфера (шар) является открытой и замкнутой.

LaTeX

$$$\mathrm{IsClopen}(\mathrm{ball}(x,r))$$$

Lean4

theorem isClopen_ball : IsClopen (ball x r) :=
  ⟨isClosed_ball x r, isOpen_ball⟩

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

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

Разделы

Аффилиация

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