isClopen_integer

Mathlib.Topology.Algebra.Valued.ValuationTopology

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

← MathLib Explorer

English

The closed unit ball { x ∈ R : v(x) ≤ 1 } is clopen, i.e., it is both open and closed.

Русский

Замкованный единичный шар является открытым и замкнутым (clopen).

LaTeX

$$IsClopen( { x ∈ R | v(x) ≤ 1 } )$$

Lean4

/-- The closed unit ball of a valued ring is clopen. -/
theorem isClopen_integer : IsClopen (_i.v.integer : Set R) :=
  ⟨isClosed_integer _, isOpen_integer _⟩

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

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

Разделы

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

Аффилиация

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