balanced_iff_smul_mem — Mathlib

English

A set s is balanced iff for every a with ||a|| ≤ 1, a·s ⊆ s.

Русский

Множество s сбалансировано тогда и только тогда, когда для каждого a с ||a|| ≤ 1 верно a·s ⊆ s.

LaTeX

$$Balanced 𝕜 s ↔ ∀ a, ||a|| ≤ 1 → a · s ⊆ s$$

Lean4

theorem balanced_iff_smul_mem : Balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s :=
  forall₂_congr fun _a _ha => smul_set_subset_iff

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