absIsAdmissible — Mathlib

English

The absolute value on integers is admissible, in a general sense, satisfying a partitioning property with a suitable card function.

Русский

Абсолютная величина на целых числах является допустимой, удовлетворяя соответствующему свойству разбиения.

LaTeX

$$AbsoluteValue.abs.IsAdmissible$$

Lean4

/-- `abs : ℤ → ℤ` is an admissible absolute value. -/
noncomputable def absIsAdmissible : IsAdmissible AbsoluteValue.abs :=
  { AbsoluteValue.abs_isEuclidean with
    card := fun ε ↦ ⌈1 / ε⌉₊
    exists_partition' := fun n _ hε _ hb ↦ exists_partition_int n hε hb }

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