isClopen_closedBall

Mathlib.Topology.Algebra.Valued.ValuationTopology

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

← MathLib Explorer

English

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

Русский

Сфера { x : R : v(x) = r } дискретна и открыта, если r ≠ 0.

LaTeX

$$$\{x : R : v(x) = r\}$ клозe и открыта; $r\neq 0$$$

Lean4

/-- A closed ball centred at the origin in a valued ring is clopen. -/
theorem isClopen_closedBall {r : Γ₀} (hr : r ≠ 0) : IsClopen (X := R) {x | v x ≤ r} :=
  ⟨isClosed_closedBall _ _, isOpen_closedBall _ hr⟩

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

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

Разделы

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

Аффилиация

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