subset_compl_ball — Mathlib

English

In a normed ring with summable geometric series, all nonunits lie outside the unit ball around 1; equivalently, ∥x−1∥ ≥ 1 for any nonunit x.

Русский

Во взгляде на нормированное кольцо с суммируемым геометрическим рядом все неединицы лежат вне шара вокруг 1 радиуса 1; то есть ∥x−1∥ ≥ 1 для любого неединичного x.

LaTeX

$$$\forall x\,(\neg IsUnit x)\Rightarrow \|x-1\| \ge 1.$$$

Lean4

/-- The `nonunits` in a normed ring with summable geometric series are contained in the
complement of the ball of radius `1` centered at `1 : R`. -/
theorem subset_compl_ball : nonunits R ⊆ (Metric.ball (1 : R) 1)ᶜ := fun x hx h₁ ↦
  hx <| sub_sub_self 1 x ▸ (Units.oneSub (1 - x) (by rwa [mem_ball_iff_norm'] at h₁)).isUnit

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