The canonical valuation of a valued ring is continuous #
A Valued R Γ₀ structure carries the topology defined by its valuation, and Valued.isOpen_ball
gives that every ball {a | v a < γ} is open. In particular the sets {a | v a < v b} cut out by
the attained values are open, which is exactly Valuation.IsContinuous for Valued.v.
Main results #
Valued.isContinuous_v: the valuation of aValuedring is continuous.
theorem
Valued.isContinuous_v
{R : Type u_1}
[Ring R]
{Γ₀ : Type u_2}
[LinearOrderedCommGroupWithZero Γ₀]
[Valued R Γ₀]
:
The valuation of a Valued ring is continuous for the topology it defines.