isClopen_closedBall

Mathlib.Topology.Algebra.Valued.ValuativeRel

URI: https://scilib.ai/kg/mathlib#IsValuativeTopology.isClopen_closedBall

English

The sphere { x : v(x) = r } is clopen for r ≠ 0.

Русский

Сфера { x : v(x) = r } для r ≠ 0 открыта и замкнута.

LaTeX

$$IsClopen( {x ∈ R | v(x) = r} )$$

Lean4

theorem isClopen_closedBall {r : ValueGroupWithZero R} (hr : r ≠ 0) : IsClopen {x | v x ≤ r} :=
  ⟨isClosed_closedBall _, isOpen_closedBall hr⟩

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

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

Разделы

Аффилиация

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