AddCircle.norm_eq
theorem AddCircle.norm_eq : ∀ (p : ℝ) {x : ℝ}, ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
This theorem states that for any real number `p` and for any `x` in the real numbers, the norm of `x` (written as `‖↑x‖`) is equal to the absolute value of `x` subtracted by the product of `p` and the nearest integer to `p⁻¹ * x`, i.e., `round (p⁻¹ * x)`, where `round` is a function that rounds a given number to the nearest integer. This result is valid in the context of a linear ordered ring and a floor ring.
More concisely: For any real number `p` and `x`, the norm of `x` equals the absolute value of `x` minus `p` times the nearest integer to `p⁻¹ * x`.
|
Mathlib.Analysis.Normed.Group.AddCircle._auxLemma.10
theorem Mathlib.Analysis.Normed.Group.AddCircle._auxLemma.10 :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.closedBall x ε) = (dist y x ≤ ε) := by
sorry
This theorem, `Mathlib.Analysis.Normed.Group.AddCircle._auxLemma.10`, asserts that for any pseudometric space `α`, any two elements `x` and `y` in this space, and any real number `ε`, the proposition that `y` belongs to the closed ball with center `x` and radius `ε` (i.e., `y ∈ Metric.closedBall x ε`) is equivalent to the statement that the distance between `y` and `x` is less than or equal to `ε` (i.e., `dist y x ≤ ε`). In other words, a point `y` is in the closed ball centered at `x` with radius `ε` in a pseudometric space if and only if the distance from `y` to `x` is not greater than `ε`.
More concisely: In a pseudometric space, an element belongs to the closed ball centered at another element with a given radius if and only if the distance between them is less than or equal to the radius.
|