isBounded_of_abs_le — Mathlib

English

For any abelian group with linear order compatible with metric, the set {x : |x| ≤ C} is bounded.

Русский

Для абелевой группы с линейным порядком, совместимым с метрикой, множество {x: |x| ≤ C} ограничено.

LaTeX

$$IsBounded({x : α | |x| ≤ C}).$$

Lean4

theorem isBounded_of_abs_le (C : α) : Bornology.IsBounded {x : α | |x| ≤ C} :=
  by
  convert Metric.isBounded_Icc (-C) C
  ext1 x
  simp [abs_le]

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