isOpen_valuationSubring — Mathlib

English

For a valued field K with valuation hv, the valuation subring hv.v.valuationSubring is an open subset of K.

Русский

Для поля K с оценкой hv, подсколо hv.v.valuationSubring является открытым подмножеством K.

LaTeX

$$$\\operatorname{IsOpen}\\left( hv.v.valuationSubring : \\{K\\} \\right)$$$

Lean4

/-- The valuation subring of a valued field is open. -/
theorem isOpen_valuationSubring (K : Type u) [Field K] [hv : Valued K Γ₀] : IsOpen (hv.v.valuationSubring : Set K) :=
  isOpen_integer K

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