isOpen_sphere — Mathlib

English

Let R be a valued ring with valuation v into Γ₀. For every r ∈ Γ₀ with r ≠ 0, the sphere centered at the origin, { x ∈ R : v(x) = r }, is an open subset of R.

Русский

Пусть R — округленное кольцо с оценкой v в Γ₀. Для каждого r ∈ Γ₀ с r ≠ 0 сфера, центрированная в начале, { x ∈ R : v(x) = r }, открыта в R.

LaTeX

$$$\\forall r \\in \\Gamma_0,\\ r \\neq 0 \\implies \\operatorname{IsOpen}\\left(\\{x \\in R \\mid v(x) = r\\}\\right)$$$

Lean4

/-- A sphere centred at the origin in a valued ring is open. -/
theorem isOpen_sphere {r : Γ₀} (hr : r ≠ 0) : IsOpen (X := R) {x | v x = r} :=
  isClopen_sphere _ hr |>.isOpen

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