isClopen_sphere

Mathlib.Topology.MetricSpace.Ultra.Basic

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

English

The sphere is clopen.

Русский

Сфера клипна (одновременно открыта и закрыта).

LaTeX

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

Lean4

theorem isClopen_sphere {r : ℝ} (hr : r ≠ 0) : IsClopen (sphere x r) :=
  ⟨Metric.isClosed_sphere, isOpen_sphere x hr⟩

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

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

Разделы

Аффилиация

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