balanced_iff_closedBall_smul — Mathlib

English

A set s is balanced if and only if the closed ball of radius 1 centered at 0, when scaled, maps s into itself.

Русский

Множество s сбалансировано тогда, когда шар с радиусом 1, умножаемый на s, остаётся внутри s.

LaTeX

$$Balanced 𝕜 s ↔ Metric.closedBall(0,1) · s ⊆ s$$

Lean4

theorem balanced_iff_closedBall_smul : Balanced 𝕜 s ↔ Metric.closedBall (0 : 𝕜) 1 • s ⊆ s := by
  simp [balanced_iff_smul_mem, smul_subset_iff]

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