Bounded and power-bounded elements of normed rings

In a seminormed ring the balls about zero form a neighbourhood basis of zero, so norm-bounded sets are bounded in the sense of TauCeti.Huber.IsBounded. For a normed division ring this identifies the power-bounded elements with the closed unit ball and shows that the ring is uniform; for instance ℚ_[p] is uniform, and its power-bounded elements are those of ℤ_[p].

Main results

• TauCeti.Huber.isBounded_closedBall_zero: closed balls about zero are bounded.
• TauCeti.Huber.isPowerBounded_iff_norm_le_one: in a normed division ring an element is power-bounded exactly when its norm is at most one.
• TauCeti.Huber.IsUniform.of_normedDivisionRing: normed division rings are uniform.

References

• Wedhorn, Adic Spaces, Definition 5.27.

@[simp]

theorem TauCeti.Huber.isBounded_closedBall_zero {R : Type u_1} [SeminormedRing R] (r : ℝ) : IsBounded (Metric.closedBall 0 r)

Closed balls about zero are bounded in a seminormed ring.

theorem TauCeti.Huber.IsPowerBounded.of_norm_le_one {R : Type u_1} [SeminormedRing R] {x : R} (hx : ‖x‖ ≤ 1) : IsPowerBounded x

An element of norm at most one in a seminormed ring is power-bounded.

@[simp]

theorem TauCeti.Huber.isPowerBounded_iff_norm_le_one {K : Type u_1} [NormedDivisionRing K] {x : K} : IsPowerBounded x ↔ ‖x‖ ≤ 1

In a normed division ring the power-bounded elements are the closed unit ball.

@[instance 100]

instance TauCeti.Huber.IsUniform.of_normedDivisionRing {K : Type u_1} [NormedDivisionRing K] : IsUniform K

Normed division rings are uniform.